{-# OPTIONS_GHC -Wunused-imports #-}

-- | Generic traversal and reduce for concrete syntax,
--   in the style of "Agda.Syntax.Internal.Generic".
--
--   However, here we use the terminology of 'Data.Traversable'.

module Agda.Syntax.Concrete.Generic where

import Data.Bifunctor
import Data.Functor

import Agda.Syntax.Common
import Agda.Syntax.Concrete

import Agda.Utils.Either
import Agda.Utils.List1 (List1)
import Agda.Utils.List2 (List2)

import Agda.Utils.Impossible

-- Generic traversals for concrete expressions.
-- ========================================================================

-- | Generic traversals for concrete expressions.
--
--   Note: does not go into patterns!
class ExprLike a where
  mapExpr :: (Expr -> Expr) -> a -> a
  -- ^ This corresponds to 'map'.

  foldExpr :: Monoid m => (Expr -> m) -> a -> m
  -- ^ This corresponds to 'foldMap'.

  traverseExpr :: Monad m => (Expr -> m Expr) -> a -> m a
  -- ^ This corresponds to 'mapM'.

  default mapExpr :: (Functor t, ExprLike b, t b ~ a) => (Expr -> Expr) -> a -> a
  mapExpr = (b -> b) -> a -> a
(b -> b) -> t b -> t b
forall a b. (a -> b) -> t a -> t b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((b -> b) -> a -> a)
-> ((Expr -> Expr) -> b -> b) -> (Expr -> Expr) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> b -> b
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr

  default foldExpr
    :: (Monoid m, Foldable t, ExprLike b, t b ~ a)
    => (Expr -> m) -> a -> m
  foldExpr = (b -> m) -> a -> m
(b -> m) -> t b -> m
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> m) -> a -> m)
-> ((Expr -> m) -> b -> m) -> (Expr -> m) -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> b -> m
forall m. Monoid m => (Expr -> m) -> b -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

  default traverseExpr
    :: (Monad m, Traversable t, ExprLike b, t b ~ a)
    => (Expr -> m Expr) -> a -> m a
  traverseExpr = (b -> m b) -> a -> m a
(b -> m b) -> t b -> m (t 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) -> t a -> f (t b)
traverse ((b -> m b) -> a -> m a)
-> ((Expr -> m Expr) -> b -> m b) -> (Expr -> m Expr) -> a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> b -> m b
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
traverseExpr


-- Instances for things that do not contain expressions.
---------------------------------------------------------------------------

instance ExprLike () where
  mapExpr :: (Expr -> Expr) -> () -> ()
mapExpr Expr -> Expr
_      = () -> ()
forall a. a -> a
id
  foldExpr :: forall m. Monoid m => (Expr -> m) -> () -> m
foldExpr Expr -> m
_ ()
_   = m
forall a. Monoid a => a
mempty
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> () -> m ()
traverseExpr Expr -> m Expr
_ = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance ExprLike Name where
  mapExpr :: (Expr -> Expr) -> Name -> Name
mapExpr Expr -> Expr
_      = Name -> Name
forall a. a -> a
id
  foldExpr :: forall m. Monoid m => (Expr -> m) -> Name -> m
foldExpr Expr -> m
_ Name
_   = m
forall a. Monoid a => a
mempty
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Name -> m Name
traverseExpr Expr -> m Expr
_ = Name -> m Name
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance ExprLike QName where
  mapExpr :: (Expr -> Expr) -> QName -> QName
mapExpr Expr -> Expr
_      = QName -> QName
forall a. a -> a
id
  foldExpr :: forall m. Monoid m => (Expr -> m) -> QName -> m
foldExpr Expr -> m
_ QName
_   = m
forall a. Monoid a => a
mempty
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> QName -> m QName
traverseExpr Expr -> m Expr
_ = QName -> m QName
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance ExprLike Bool where
  mapExpr :: (Expr -> Expr) -> Bool -> Bool
mapExpr Expr -> Expr
_      = Bool -> Bool
forall a. a -> a
id
  foldExpr :: forall m. Monoid m => (Expr -> m) -> Bool -> m
foldExpr Expr -> m
_ Bool
_   = m
forall a. Monoid a => a
mempty
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Bool -> m Bool
traverseExpr Expr -> m Expr
_ = Bool -> m Bool
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return

-- Instances for collections and decorations.
---------------------------------------------------------------------------

instance ExprLike a => ExprLike [a]
instance ExprLike a => ExprLike (List1 a)
instance ExprLike a => ExprLike (List2 a)
instance ExprLike a => ExprLike (Maybe a)

instance ExprLike a => ExprLike (Arg a)
instance ExprLike a => ExprLike (Named name a)
instance ExprLike a => ExprLike (Ranged a)
instance ExprLike a => ExprLike (WithHiding a)

instance ExprLike a => ExprLike (MaybePlaceholder a)
instance ExprLike a => ExprLike (RHS' a)
instance ExprLike a => ExprLike (TacticAttribute' a)
instance ExprLike a => ExprLike (TypedBinding' a)
instance ExprLike a => ExprLike (WhereClause' a)

instance (ExprLike a, ExprLike b) => ExprLike (Either a b) where
  mapExpr :: (Expr -> Expr) -> Either a b -> Either a b
mapExpr Expr -> Expr
f      = (a -> a) -> (b -> b) -> Either a b -> Either a b
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ((Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f) ((Expr -> Expr) -> b -> b
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f)
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> Either a b -> m (Either a b)
traverseExpr Expr -> m Expr
f = (a -> m a) -> (b -> m b) -> Either a b -> m (Either a b)
forall (f :: * -> *) a c b d.
Functor f =>
(a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
traverseEither ((Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f) ((Expr -> m Expr) -> b -> m b
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
traverseExpr Expr -> m Expr
f)
  foldExpr :: forall m. Monoid m => (Expr -> m) -> Either a b -> m
foldExpr Expr -> m
f     = (a -> m) -> (b -> m) -> Either a b -> m
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Expr -> m) -> a -> m
forall m. Monoid m => (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f) ((Expr -> m) -> b -> m
forall m. Monoid m => (Expr -> m) -> b -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f)

instance (ExprLike a, ExprLike b) => ExprLike (a, b) where
  mapExpr :: (Expr -> Expr) -> (a, b) -> (a, b)
mapExpr      Expr -> Expr
f (a
x, b
y) = ((Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
x, (Expr -> Expr) -> b -> b
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f b
y)
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> (a, b) -> m (a, b)
traverseExpr Expr -> m Expr
f (a
x, b
y) = (,) (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f a
x m (b -> (a, b)) -> m b -> m (a, b)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> m Expr) -> b -> m b
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
traverseExpr Expr -> m Expr
f b
y
  foldExpr :: forall m. Monoid m => (Expr -> m) -> (a, b) -> m
foldExpr     Expr -> m
f (a
x, b
y) = (Expr -> m) -> a -> m
forall m. Monoid m => (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f a
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Expr -> m) -> b -> m
forall m. Monoid m => (Expr -> m) -> b -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f b
y

instance (ExprLike a, ExprLike b, ExprLike c) => ExprLike (a, b, c) where
  mapExpr :: (Expr -> Expr) -> (a, b, c) -> (a, b, c)
mapExpr      Expr -> Expr
f (a
x, b
y, c
z) = ((Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
x, (Expr -> Expr) -> b -> b
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f b
y, (Expr -> Expr) -> c -> c
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f c
z)
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> (a, b, c) -> m (a, b, c)
traverseExpr Expr -> m Expr
f (a
x, b
y, c
z) = (,,) (a -> b -> c -> (a, b, c)) -> m a -> m (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f a
x m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> m Expr) -> b -> m b
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
traverseExpr Expr -> m Expr
f b
y m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> m Expr) -> c -> m c
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> c -> m c
traverseExpr Expr -> m Expr
f c
z
  foldExpr :: forall m. Monoid m => (Expr -> m) -> (a, b, c) -> m
foldExpr     Expr -> m
f (a
x, b
y, c
z) = (Expr -> m) -> a -> m
forall m. Monoid m => (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f a
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Expr -> m) -> b -> m
forall m. Monoid m => (Expr -> m) -> b -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f b
y m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Expr -> m) -> c -> m
forall m. Monoid m => (Expr -> m) -> c -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f c
z

instance (ExprLike a, ExprLike b, ExprLike c, ExprLike d) => ExprLike (a, b, c, d) where
  mapExpr :: (Expr -> Expr) -> (a, b, c, d) -> (a, b, c, d)
mapExpr      Expr -> Expr
f (a
x, b
y, c
z, d
w) = ((Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
x, (Expr -> Expr) -> b -> b
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f b
y, (Expr -> Expr) -> c -> c
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f c
z, (Expr -> Expr) -> d -> d
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f d
w)
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> (a, b, c, d) -> m (a, b, c, d)
traverseExpr Expr -> m Expr
f (a
x, b
y, c
z, d
w) = (,,,) (a -> b -> c -> d -> (a, b, c, d))
-> m a -> m (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f a
x m (b -> c -> d -> (a, b, c, d))
-> m b -> m (c -> d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> m Expr) -> b -> m b
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> b -> m b
traverseExpr Expr -> m Expr
f b
y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> m Expr) -> c -> m c
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> c -> m c
traverseExpr Expr -> m Expr
f c
z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> m Expr) -> d -> m d
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> d -> m d
traverseExpr Expr -> m Expr
f d
w
  foldExpr :: forall m. Monoid m => (Expr -> m) -> (a, b, c, d) -> m
foldExpr     Expr -> m
f (a
x, b
y, c
z, d
w) = (Expr -> m) -> a -> m
forall m. Monoid m => (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f a
x m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Expr -> m) -> b -> m
forall m. Monoid m => (Expr -> m) -> b -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f b
y m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Expr -> m) -> c -> m
forall m. Monoid m => (Expr -> m) -> c -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f c
z m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` (Expr -> m) -> d -> m
forall m. Monoid m => (Expr -> m) -> d -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f d
w

-- Interesting instances
---------------------------------------------------------------------------

instance ExprLike Expr where
  mapExpr :: (Expr -> Expr) -> Expr -> Expr
mapExpr Expr -> Expr
f Expr
e0 = case Expr
e0 of
     Ident{}                 -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     Lit{}                   -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     QuestionMark{}          -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     Underscore{}            -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     RawApp Range
r List2 Expr
es             -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> List2 Expr -> Expr
RawApp Range
r               (List2 Expr -> Expr) -> List2 Expr -> Expr
forall a b. (a -> b) -> a -> b
$ List2 Expr -> List2 Expr
forall e. ExprLike e => e -> e
mapE List2 Expr
es
     App Range
r Expr
e NamedArg Expr
es              -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> NamedArg Expr -> Expr
App Range
r       (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)   (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> NamedArg Expr
forall e. ExprLike e => e -> e
mapE NamedArg Expr
es
     OpApp Range
r QName
q Set Name
ns OpAppArgs
es         -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> QName -> Set Name -> OpAppArgs -> Expr
OpApp Range
r QName
q Set Name
ns           (OpAppArgs -> Expr) -> OpAppArgs -> Expr
forall a b. (a -> b) -> a -> b
$ OpAppArgs -> OpAppArgs
forall e. ExprLike e => e -> e
mapE OpAppArgs
es
     WithApp Range
r Expr
e [Expr]
es          -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> [Expr] -> Expr
WithApp Range
r   (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)   ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> [Expr]
forall e. ExprLike e => e -> e
mapE [Expr]
es
     HiddenArg Range
r Named_ Expr
e           -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Named_ Expr -> Expr
HiddenArg Range
r            (Named_ Expr -> Expr) -> Named_ Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Named_ Expr
forall e. ExprLike e => e -> e
mapE Named_ Expr
e
     InstanceArg Range
r Named_ Expr
e         -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Named_ Expr -> Expr
InstanceArg Range
r          (Named_ Expr -> Expr) -> Named_ Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Named_ Expr
forall e. ExprLike e => e -> e
mapE Named_ Expr
e
     Lam Range
r List1 LamBinding
bs Expr
e              -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> List1 LamBinding -> Expr -> Expr
Lam Range
r       (List1 LamBinding -> List1 LamBinding
forall e. ExprLike e => e -> e
mapE List1 LamBinding
bs)  (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     AbsurdLam{}             -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     ExtendedLam Range
r Erased
e List1 LamClause
cs      -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Erased -> List1 LamClause -> Expr
ExtendedLam Range
r Erased
e        (List1 LamClause -> Expr) -> List1 LamClause -> Expr
forall a b. (a -> b) -> a -> b
$ List1 LamClause -> List1 LamClause
forall e. ExprLike e => e -> e
mapE List1 LamClause
cs
     Fun Range
r Arg Expr
a Expr
b               -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Arg Expr -> Expr -> Expr
Fun Range
r     (Expr -> Expr
forall e. ExprLike e => e -> e
mapE (Expr -> Expr) -> Arg Expr -> Arg Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Expr
a) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
b
     Pi Telescope1
tel Expr
e                -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope1 -> Expr -> Expr
Pi          (Telescope1 -> Telescope1
forall e. ExprLike e => e -> e
mapE Telescope1
tel) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     Rec Range
r RecordAssignments
es                -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> RecordAssignments -> Expr
Rec Range
r                  (RecordAssignments -> Expr) -> RecordAssignments -> Expr
forall a b. (a -> b) -> a -> b
$ RecordAssignments -> RecordAssignments
forall e. ExprLike e => e -> e
mapE RecordAssignments
es
     RecUpdate Range
r Expr
e [FieldAssignment]
es        -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> [FieldAssignment] -> Expr
RecUpdate Range
r (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)   ([FieldAssignment] -> Expr) -> [FieldAssignment] -> Expr
forall a b. (a -> b) -> a -> b
$ [FieldAssignment] -> [FieldAssignment]
forall e. ExprLike e => e -> e
mapE [FieldAssignment]
es
     Let Range
r List1 Declaration
ds Maybe Expr
e              -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> List1 Declaration -> Maybe Expr -> Expr
Let Range
r       (List1 Declaration -> List1 Declaration
forall e. ExprLike e => e -> e
mapE List1 Declaration
ds)  (Maybe Expr -> Expr) -> Maybe Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Maybe Expr -> Maybe Expr
forall e. ExprLike e => e -> e
mapE Maybe Expr
e
     Paren Range
r Expr
e               -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
Paren Range
r                (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     IdiomBrackets Range
r [Expr]
es      -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> [Expr] -> Expr
IdiomBrackets Range
r        ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> [Expr]
forall e. ExprLike e => e -> e
mapE [Expr]
es
     DoBlock Range
r List1 DoStmt
ss            -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> List1 DoStmt -> Expr
DoBlock Range
r              (List1 DoStmt -> Expr) -> List1 DoStmt -> Expr
forall a b. (a -> b) -> a -> b
$ List1 DoStmt -> List1 DoStmt
forall e. ExprLike e => e -> e
mapE List1 DoStmt
ss
     Absurd{}                -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     As Range
r Name
x Expr
e                -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Name -> Expr -> Expr
As Range
r Name
x                 (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     Dot Range
r Expr
e                 -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
Dot Range
r                  (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     DoubleDot Range
r Expr
e           -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
DoubleDot Range
r            (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     Tactic Range
r Expr
e              -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
Tactic Range
r     (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)
     Quote{}                 -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     QuoteTerm{}             -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     Unquote{}               -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     DontCare Expr
e              -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
DontCare               (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     Equal{}                 -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     Ellipsis{}              -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     Generalized Expr
e           -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Generalized            (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     KnownIdent{}            -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     KnownOpApp NameKind
nk Range
r QName
q Set Name
ns OpAppArgs
es -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ NameKind -> Range -> QName -> Set Name -> OpAppArgs -> Expr
KnownOpApp NameKind
nk Range
r QName
q Set Name
ns   (OpAppArgs -> Expr) -> OpAppArgs -> Expr
forall a b. (a -> b) -> a -> b
$ OpAppArgs -> OpAppArgs
forall e. ExprLike e => e -> e
mapE OpAppArgs
es
   where
     mapE :: ExprLike e => e -> e
     mapE :: forall e. ExprLike e => e -> e
mapE = (Expr -> Expr) -> e -> e
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f

  foldExpr :: forall m. Monoid m => (Expr -> m) -> Expr -> m
foldExpr     = (Expr -> m) -> Expr -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
traverseExpr = (Expr -> m Expr) -> Expr -> m Expr
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ExprLike FieldAssignment where
  mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment
mapExpr      Expr -> Expr
f (FieldAssignment Name
x Expr
e) = Name -> Expr -> FieldAssignment
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x ((Expr -> Expr) -> Expr -> Expr
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f Expr
e)
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> FieldAssignment -> m FieldAssignment
traverseExpr Expr -> m Expr
f (FieldAssignment Name
x Expr
e) = (\Expr
e' -> Name -> Expr -> FieldAssignment
forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x Expr
e') (Expr -> FieldAssignment) -> m Expr -> m FieldAssignment
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr) -> Expr -> m Expr
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Expr -> m Expr
traverseExpr Expr -> m Expr
f Expr
e
  foldExpr :: forall m. Monoid m => (Expr -> m) -> FieldAssignment -> m
foldExpr     Expr -> m
f (FieldAssignment Name
_ Expr
e) = (Expr -> m) -> Expr -> m
forall m. Monoid m => (Expr -> m) -> Expr -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f Expr
e

instance ExprLike ModuleAssignment where
  mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment
mapExpr      Expr -> Expr
f (ModuleAssignment QName
m [Expr]
es ImportDirective
i) = QName -> [Expr] -> ImportDirective -> ModuleAssignment
ModuleAssignment QName
m ((Expr -> Expr) -> [Expr] -> [Expr]
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f [Expr]
es) ImportDirective
i
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment
traverseExpr Expr -> m Expr
f (ModuleAssignment QName
m [Expr]
es ImportDirective
i) = (\[Expr]
es' -> QName -> [Expr] -> ImportDirective -> ModuleAssignment
ModuleAssignment QName
m [Expr]
es' ImportDirective
i) ([Expr] -> ModuleAssignment) -> m [Expr] -> m ModuleAssignment
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> m Expr) -> [Expr] -> m [Expr]
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> [Expr] -> m [Expr]
traverseExpr Expr -> m Expr
f [Expr]
es
  foldExpr :: forall m. Monoid m => (Expr -> m) -> ModuleAssignment -> m
foldExpr     Expr -> m
f (ModuleAssignment QName
m [Expr]
es ImportDirective
i) = (Expr -> m) -> [Expr] -> m
forall m. Monoid m => (Expr -> m) -> [Expr] -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f [Expr]
es

instance ExprLike a => ExprLike (OpApp a) where
  mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a
mapExpr Expr -> Expr
f = \case
     SyntaxBindingLambda Range
r List1 LamBinding
bs a
e -> Range -> List1 LamBinding -> a -> OpApp a
forall e. Range -> List1 LamBinding -> e -> OpApp e
SyntaxBindingLambda Range
r (List1 LamBinding -> List1 LamBinding
forall e. ExprLike e => e -> e
mapE List1 LamBinding
bs) (a -> OpApp a) -> a -> OpApp a
forall a b. (a -> b) -> a -> b
$ a -> a
forall e. ExprLike e => e -> e
mapE a
e
     Ordinary                 a
e -> a -> OpApp a
forall e. e -> OpApp e
Ordinary                        (a -> OpApp a) -> a -> OpApp a
forall a b. (a -> b) -> a -> b
$ a -> a
forall e. ExprLike e => e -> e
mapE a
e
   where
     mapE :: ExprLike e => e -> e
     mapE :: forall e. ExprLike e => e -> e
mapE = (Expr -> Expr) -> e -> e
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f
  foldExpr :: forall m. Monoid m => (Expr -> m) -> OpApp a -> m
foldExpr     = (Expr -> m) -> OpApp a -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> OpApp a -> m (OpApp a)
traverseExpr = (Expr -> m Expr) -> OpApp a -> m (OpApp a)
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ExprLike LamBinding where
  mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding
mapExpr Expr -> Expr
f = \case
     e :: LamBinding
e@DomainFree{}-> LamBinding
e
     DomainFull TypedBinding' Expr
bs -> TypedBinding' Expr -> LamBinding
forall a. a -> LamBinding' a
DomainFull (TypedBinding' Expr -> LamBinding)
-> TypedBinding' Expr -> LamBinding
forall a b. (a -> b) -> a -> b
$ TypedBinding' Expr -> TypedBinding' Expr
mapE TypedBinding' Expr
bs
   where mapE :: TypedBinding' Expr -> TypedBinding' Expr
mapE TypedBinding' Expr
e = (Expr -> Expr) -> TypedBinding' Expr -> TypedBinding' Expr
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f TypedBinding' Expr
e
  foldExpr :: forall m. Monoid m => (Expr -> m) -> LamBinding -> m
foldExpr     = (Expr -> m) -> LamBinding -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> LamBinding -> m LamBinding
traverseExpr = (Expr -> m Expr) -> LamBinding -> m LamBinding
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ExprLike LHS where
  mapExpr :: (Expr -> Expr) -> LHS -> LHS
mapExpr Expr -> Expr
f = \case
     LHS Pattern
ps [RewriteEqn]
res [WithExpr]
wes -> Pattern -> [RewriteEqn] -> [WithExpr] -> LHS
LHS Pattern
ps ([RewriteEqn] -> [RewriteEqn]
forall e. ExprLike e => e -> e
mapE [RewriteEqn]
res) ([WithExpr] -> [WithExpr]
forall e. ExprLike e => e -> e
mapE [WithExpr]
wes)
   where
     mapE :: ExprLike a => a -> a
     mapE :: forall e. ExprLike e => e -> e
mapE = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f
  foldExpr :: forall m. Monoid m => (Expr -> m) -> LHS -> m
foldExpr     = (Expr -> m) -> LHS -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> LHS -> m LHS
traverseExpr = (Expr -> m Expr) -> LHS -> m LHS
forall a. HasCallStack => a
__IMPOSSIBLE__

instance (ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) where
  mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e
mapExpr Expr -> Expr
f = \case
    Rewrite List1 (qn, e)
es    -> List1 (qn, e) -> RewriteEqn' qn nm p e
forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
Rewrite ((Expr -> Expr) -> List1 (qn, e) -> List1 (qn, e)
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f List1 (qn, e)
es)
    Invert qn
qn List1 (Named nm (p, e))
pes -> qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
forall qn nm p e.
qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
Invert qn
qn (List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e)
-> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
forall a b. (a -> b) -> a -> b
$ ((Named nm (p, e) -> Named nm (p, e))
-> List1 (Named nm (p, e)) -> List1 (Named nm (p, e))
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named nm (p, e) -> Named nm (p, e))
 -> List1 (Named nm (p, e)) -> List1 (Named nm (p, e)))
-> ((Expr -> Expr) -> Named nm (p, e) -> Named nm (p, e))
-> (Expr -> Expr)
-> List1 (Named nm (p, e))
-> List1 (Named nm (p, e))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((p, e) -> (p, e)) -> Named nm (p, e) -> Named nm (p, e)
forall a b. (a -> b) -> Named nm a -> Named nm b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((p, e) -> (p, e)) -> Named nm (p, e) -> Named nm (p, e))
-> ((Expr -> Expr) -> (p, e) -> (p, e))
-> (Expr -> Expr)
-> Named nm (p, e)
-> Named nm (p, e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> e) -> (p, e) -> (p, e)
forall a b. (a -> b) -> (p, a) -> (p, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((e -> e) -> (p, e) -> (p, e))
-> ((Expr -> Expr) -> e -> e) -> (Expr -> Expr) -> (p, e) -> (p, e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> e -> e
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr) Expr -> Expr
f List1 (Named nm (p, e))
pes
    LeftLet List1 (p, e)
pes   -> List1 (p, e) -> RewriteEqn' qn nm p e
forall qn nm p e. List1 (p, e) -> RewriteEqn' qn nm p e
LeftLet (List1 (p, e) -> RewriteEqn' qn nm p e)
-> List1 (p, e) -> RewriteEqn' qn nm p e
forall a b. (a -> b) -> a -> b
$ (((p, e) -> (p, e)) -> List1 (p, e) -> List1 (p, e)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((p, e) -> (p, e)) -> List1 (p, e) -> List1 (p, e))
-> ((Expr -> Expr) -> (p, e) -> (p, e))
-> (Expr -> Expr)
-> List1 (p, e)
-> List1 (p, e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> e) -> (p, e) -> (p, e)
forall a b. (a -> b) -> (p, a) -> (p, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((e -> e) -> (p, e) -> (p, e))
-> ((Expr -> Expr) -> e -> e) -> (Expr -> Expr) -> (p, e) -> (p, e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> e -> e
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr) Expr -> Expr
f List1 (p, e)
pes
  foldExpr :: forall m. Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m
foldExpr     = (Expr -> m) -> RewriteEqn' qn nm p e -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr)
-> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e)
traverseExpr = (Expr -> m Expr)
-> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e)
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ExprLike LamClause where
  mapExpr :: (Expr -> Expr) -> LamClause -> LamClause
mapExpr Expr -> Expr
f (LamClause [Pattern]
ps RHS
rhs Bool
ca) = [Pattern] -> RHS -> Bool -> LamClause
LamClause [Pattern]
ps ((Expr -> Expr) -> RHS -> RHS
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f RHS
rhs) Bool
ca
  foldExpr :: forall m. Monoid m => (Expr -> m) -> LamClause -> m
foldExpr     = (Expr -> m) -> LamClause -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> LamClause -> m LamClause
traverseExpr = (Expr -> m Expr) -> LamClause -> m LamClause
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ExprLike DoStmt where
  mapExpr :: (Expr -> Expr) -> DoStmt -> DoStmt
mapExpr Expr -> Expr
f (DoBind Range
r Pattern
p Expr
e [LamClause]
cs) = Range -> Pattern -> Expr -> [LamClause] -> DoStmt
DoBind Range
r Pattern
p ((Expr -> Expr) -> Expr -> Expr
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f Expr
e) ((Expr -> Expr) -> [LamClause] -> [LamClause]
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f [LamClause]
cs)
  mapExpr Expr -> Expr
f (DoThen Expr
e)        = Expr -> DoStmt
DoThen ((Expr -> Expr) -> Expr -> Expr
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f Expr
e)
  mapExpr Expr -> Expr
f (DoLet Range
r List1 Declaration
ds)      = Range -> List1 Declaration -> DoStmt
DoLet Range
r ((Expr -> Expr) -> List1 Declaration -> List1 Declaration
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f List1 Declaration
ds)

  foldExpr :: forall m. Monoid m => (Expr -> m) -> DoStmt -> m
foldExpr     = (Expr -> m) -> DoStmt -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> DoStmt -> m DoStmt
traverseExpr = (Expr -> m Expr) -> DoStmt -> m DoStmt
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ExprLike ModuleApplication where
  mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication
mapExpr Expr -> Expr
f = \case
     SectionApp Range
r Telescope
bs Expr
e -> Range -> Telescope -> Expr -> ModuleApplication
SectionApp Range
r (Telescope -> Telescope
forall e. ExprLike e => e -> e
mapE Telescope
bs) (Expr -> ModuleApplication) -> Expr -> ModuleApplication
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     e :: ModuleApplication
e@RecordModuleInstance{} -> ModuleApplication
e
   where
     mapE :: ExprLike e => e -> e
     mapE :: forall e. ExprLike e => e -> e
mapE = (Expr -> Expr) -> e -> e
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f
  foldExpr :: forall m. Monoid m => (Expr -> m) -> ModuleApplication -> m
foldExpr     = (Expr -> m) -> ModuleApplication -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> ModuleApplication -> m ModuleApplication
traverseExpr = (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication
forall a. HasCallStack => a
__IMPOSSIBLE__

instance ExprLike Declaration where
  mapExpr :: (Expr -> Expr) -> Declaration -> Declaration
mapExpr Expr -> Expr
f = \case
     TypeSig ArgInfo
ai TacticAttribute
t Name
x Expr
e          -> ArgInfo -> TacticAttribute -> Name -> Expr -> Declaration
TypeSig ArgInfo
ai (TacticAttribute -> TacticAttribute
forall e. ExprLike e => e -> e
mapE TacticAttribute
t) Name
x (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)
     FieldSig IsInstance
i TacticAttribute
t Name
n Arg Expr
e          -> IsInstance -> TacticAttribute -> Name -> Arg Expr -> Declaration
FieldSig IsInstance
i (TacticAttribute -> TacticAttribute
forall e. ExprLike e => e -> e
mapE TacticAttribute
t) Name
n (Arg Expr -> Arg Expr
forall e. ExprLike e => e -> e
mapE Arg Expr
e)
     Field KwRange
r [Declaration]
fs                -> KwRange -> [Declaration] -> Declaration
Field KwRange
r                              ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ (Declaration -> Declaration) -> [Declaration] -> [Declaration]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Expr) -> Declaration -> Declaration
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f) [Declaration]
fs
     FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca   -> LHS -> RHS -> WhereClause -> Bool -> Declaration
FunClause (LHS -> LHS
forall e. ExprLike e => e -> e
mapE LHS
lhs) (RHS -> RHS
forall e. ExprLike e => e -> e
mapE RHS
rhs) (WhereClause -> WhereClause
forall e. ExprLike e => e -> e
mapE WhereClause
wh) (Bool -> Bool
forall e. ExprLike e => e -> e
mapE Bool
ca)
     DataSig Range
r Erased
er Name
x [LamBinding]
bs Expr
e       -> Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
DataSig Range
r Erased
er Name
x ([LamBinding] -> [LamBinding]
forall e. ExprLike e => e -> e
mapE [LamBinding]
bs)             (Expr -> Declaration) -> Expr -> Declaration
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     DataDef Range
r Name
n [LamBinding]
bs [Declaration]
cs         -> Range -> Name -> [LamBinding] -> [Declaration] -> Declaration
DataDef Range
r Name
n ([LamBinding] -> [LamBinding]
forall e. ExprLike e => e -> e
mapE [LamBinding]
bs)                ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
cs
     Data Range
r Erased
er Name
n [LamBinding]
bs Expr
e [Declaration]
cs       -> Range
-> Erased
-> Name
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
Data Range
r Erased
er Name
n ([LamBinding] -> [LamBinding]
forall e. ExprLike e => e -> e
mapE [LamBinding]
bs) (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)       ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
cs
     RecordSig Range
r Erased
er Name
ind [LamBinding]
bs Expr
e   -> Range -> Erased -> Name -> [LamBinding] -> Expr -> Declaration
RecordSig Range
r Erased
er Name
ind ([LamBinding] -> [LamBinding]
forall e. ExprLike e => e -> e
mapE [LamBinding]
bs)         (Expr -> Declaration) -> Expr -> Declaration
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e
     RecordDef Range
r Name
n [RecordDirective]
dir [LamBinding]
tel [Declaration]
ds  -> Range
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Name
n [RecordDirective]
dir ([LamBinding] -> [LamBinding]
forall e. ExprLike e => e -> e
mapE [LamBinding]
tel)         ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Record Range
r Erased
er Name
n [RecordDirective]
dir [LamBinding]
tel Expr
e [Declaration]
ds
                               -> Range
-> Erased
-> Name
-> [RecordDirective]
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
Record Range
r Erased
er Name
n [RecordDirective]
dir ([LamBinding] -> [LamBinding]
forall e. ExprLike e => e -> e
mapE [LamBinding]
tel) (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)
                                                                       ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     e :: Declaration
e@Infix{}                 -> Declaration
e
     e :: Declaration
e@Syntax{}                -> Declaration
e
     e :: Declaration
e@PatternSyn{}            -> Declaration
e
     Mutual    KwRange
r [Declaration]
ds            -> KwRange -> [Declaration] -> Declaration
Mutual    KwRange
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     InterleavedMutual KwRange
r [Declaration]
ds    -> KwRange -> [Declaration] -> Declaration
InterleavedMutual KwRange
r                  ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     LoneConstructor KwRange
r [Declaration]
ds      -> KwRange -> [Declaration] -> Declaration
LoneConstructor KwRange
r                    ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Abstract  KwRange
r [Declaration]
ds            -> KwRange -> [Declaration] -> Declaration
Abstract  KwRange
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Private   KwRange
r Origin
o [Declaration]
ds          -> KwRange -> Origin -> [Declaration] -> Declaration
Private   KwRange
r Origin
o                        ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     InstanceB KwRange
r [Declaration]
ds            -> KwRange -> [Declaration] -> Declaration
InstanceB KwRange
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Macro     KwRange
r [Declaration]
ds            -> KwRange -> [Declaration] -> Declaration
Macro     KwRange
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Postulate KwRange
r [Declaration]
ds            -> KwRange -> [Declaration] -> Declaration
Postulate KwRange
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Primitive KwRange
r [Declaration]
ds            -> KwRange -> [Declaration] -> Declaration
Primitive KwRange
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Generalize KwRange
r [Declaration]
ds           -> KwRange -> [Declaration] -> Declaration
Generalize KwRange
r                         ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     Opaque  KwRange
r [Declaration]
ds              -> KwRange -> [Declaration] -> Declaration
Opaque KwRange
r                             ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     e :: Declaration
e@Open{}                  -> Declaration
e
     e :: Declaration
e@Import{}                -> Declaration
e
     ModuleMacro Range
r Erased
e Name
n ModuleApplication
es OpenShortHand
op ImportDirective
dir
                               -> Range
-> Erased
-> Name
-> ModuleApplication
-> OpenShortHand
-> ImportDirective
-> Declaration
ModuleMacro Range
r Erased
e Name
n (ModuleApplication -> ModuleApplication
forall e. ExprLike e => e -> e
mapE ModuleApplication
es) OpenShortHand
op ImportDirective
dir
     Module Range
r Erased
e QName
n Telescope
tel [Declaration]
ds       -> Range
-> Erased -> QName -> Telescope -> [Declaration] -> Declaration
Module Range
r Erased
e QName
n (Telescope -> Telescope
forall e. ExprLike e => e -> e
mapE Telescope
tel)              ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall e. ExprLike e => e -> e
mapE [Declaration]
ds
     UnquoteDecl Range
r [Name]
x Expr
e         -> Range -> [Name] -> Expr -> Declaration
UnquoteDecl Range
r [Name]
x (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)
     UnquoteDef Range
r [Name]
x Expr
e          -> Range -> [Name] -> Expr -> Declaration
UnquoteDef Range
r [Name]
x (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)
     UnquoteData Range
r Name
x [Name]
xs Expr
e      -> Range -> Name -> [Name] -> Expr -> Declaration
UnquoteData Range
r Name
x [Name]
xs (Expr -> Expr
forall e. ExprLike e => e -> e
mapE Expr
e)
     e :: Declaration
e@Pragma{}                -> Declaration
e
     e :: Declaration
e@Unfolding{}             -> Declaration
e
   where
     mapE :: ExprLike e => e -> e
     mapE :: forall e. ExprLike e => e -> e
mapE = (Expr -> Expr) -> e -> e
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f

  foldExpr :: forall m. Monoid m => (Expr -> m) -> Declaration -> m
foldExpr     = (Expr -> m) -> Declaration -> m
forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> Declaration -> m Declaration
traverseExpr = (Expr -> m Expr) -> Declaration -> m Declaration
forall a. HasCallStack => a
__IMPOSSIBLE__


{- Template

instance ExprLike a where
  mapExpr f = \case
    where mapE e = mapExpr f e
  foldExpr     = __IMPOSSIBLE__
  traverseExpr = __IMPOSSIBLE__

-}

-- Generic traversals for concrete declarations.
-- ========================================================================

class FoldDecl a where

  -- | Collect declarations and subdeclarations, transitively.
  -- Prefix-order tree traversal.
  foldDecl :: Monoid m => (Declaration -> m) -> a -> m

  default foldDecl :: (Monoid m, Foldable t, FoldDecl b, t b ~ a)
    => (Declaration -> m) -> a -> m
  foldDecl = (b -> m) -> a -> m
(b -> m) -> t b -> m
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> m) -> a -> m)
-> ((Declaration -> m) -> b -> m) -> (Declaration -> m) -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Declaration -> m) -> b -> m
forall m. Monoid m => (Declaration -> m) -> b -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl

instance FoldDecl a => FoldDecl [a]
instance FoldDecl a => FoldDecl (List1 a)
instance FoldDecl a => FoldDecl (List2 a)
instance FoldDecl a => FoldDecl (WhereClause' a)

instance FoldDecl Declaration where
  foldDecl :: forall m. Monoid m => (Declaration -> m) -> Declaration -> m
foldDecl Declaration -> m
f Declaration
d = Declaration -> m
f Declaration
d m -> m -> m
forall a. Semigroup a => a -> a -> a
<> case Declaration
d of
    Private  KwRange
_ Origin
_        [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    Abstract KwRange
_          [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    InstanceB KwRange
_         [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    InterleavedMutual KwRange
_ [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    LoneConstructor KwRange
_   [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    Mutual KwRange
_            [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    Module Range
_ Erased
_ QName
_ Telescope
_      [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    Macro KwRange
_             [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    Record Range
_ Erased
_ Name
_ [RecordDirective]
_ [LamBinding]
_ Expr
_  [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    RecordDef Range
_ Name
_ [RecordDirective]
_ [LamBinding]
_   [Declaration]
ds  -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    TypeSig ArgInfo
_ TacticAttribute
_ Name
_ Expr
_         -> m
forall a. Monoid a => a
mempty
    FieldSig IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_        -> m
forall a. Monoid a => a
mempty
    Generalize KwRange
_ [Declaration]
_          -> m
forall a. Monoid a => a
mempty
    Field KwRange
_ [Declaration]
_               -> m
forall a. Monoid a => a
mempty
    FunClause LHS
_ RHS
_ WhereClause
wh Bool
_      -> (Declaration -> m) -> WhereClause -> m
forall m. Monoid m => (Declaration -> m) -> WhereClause -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f WhereClause
wh
    DataSig Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_       -> m
forall a. Monoid a => a
mempty
    Data Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_ [Declaration]
_        -> m
forall a. Monoid a => a
mempty
    DataDef Range
_ Name
_ [LamBinding]
_ [Declaration]
_         -> m
forall a. Monoid a => a
mempty
    RecordSig Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_     -> m
forall a. Monoid a => a
mempty
    Infix Fixity
_ List1 Name
_               -> m
forall a. Monoid a => a
mempty
    Syntax Name
_ Notation
_              -> m
forall a. Monoid a => a
mempty
    PatternSyn Range
_ Name
_ [WithHiding Name]
_ Pattern
_      -> m
forall a. Monoid a => a
mempty
    Postulate KwRange
_ [Declaration]
_           -> m
forall a. Monoid a => a
mempty
    Primitive KwRange
_ [Declaration]
_           -> m
forall a. Monoid a => a
mempty
    Open Range
_ QName
_ ImportDirective
_              -> m
forall a. Monoid a => a
mempty
    Import Range
_ QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_        -> m
forall a. Monoid a => a
mempty
    ModuleMacro Range
_ Erased
_ Name
_ ModuleApplication
_ OpenShortHand
_ ImportDirective
_ -> m
forall a. Monoid a => a
mempty
    UnquoteDecl Range
_ [Name]
_ Expr
_       -> m
forall a. Monoid a => a
mempty
    UnquoteDef Range
_ [Name]
_ Expr
_        -> m
forall a. Monoid a => a
mempty
    UnquoteData Range
_ Name
_ [Name]
_ Expr
_     -> m
forall a. Monoid a => a
mempty
    Pragma Pragma
_                -> m
forall a. Monoid a => a
mempty
    Opaque KwRange
_ [Declaration]
ds             -> (Declaration -> m) -> [Declaration] -> m
forall m. Monoid m => (Declaration -> m) -> [Declaration] -> m
forall a m. (FoldDecl a, Monoid m) => (Declaration -> m) -> a -> m
foldDecl Declaration -> m
f [Declaration]
ds
    Unfolding KwRange
_ [QName]
_           -> m
forall a. Monoid a => a
mempty

class TraverseDecl a where

  -- | Update declarations and their subdeclarations.
  -- Prefix-order traversal: traverses subdeclarations of updated declaration.
  --
  preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> a -> m a

  default preTraverseDecl :: (Monad m, Traversable t, TraverseDecl b, t b ~ a)
    => (Declaration -> m Declaration) -> a -> m a
  preTraverseDecl = (b -> m b) -> a -> m a
(b -> m b) -> t b -> m (t 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) -> t a -> f (t b)
traverse ((b -> m b) -> a -> m a)
-> ((Declaration -> m Declaration) -> b -> m b)
-> (Declaration -> m Declaration)
-> a
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Declaration -> m Declaration) -> b -> m b
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> b -> m b
preTraverseDecl

instance TraverseDecl a => TraverseDecl [a]
instance TraverseDecl a => TraverseDecl (List1 a)
instance TraverseDecl a => TraverseDecl (List2 a)
instance TraverseDecl a => TraverseDecl (WhereClause' a)

instance TraverseDecl Declaration where
  preTraverseDecl :: forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> Declaration -> m Declaration
preTraverseDecl Declaration -> m Declaration
f Declaration
d0 = do
    d <- Declaration -> m Declaration
f Declaration
d0
    case d of
      Private  KwRange
r Origin
o        [Declaration]
ds     -> KwRange -> Origin -> [Declaration] -> Declaration
Private KwRange
r Origin
o             ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      Abstract KwRange
r          [Declaration]
ds     -> KwRange -> [Declaration] -> Declaration
Abstract KwRange
r              ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      InstanceB KwRange
r         [Declaration]
ds     -> KwRange -> [Declaration] -> Declaration
InstanceB KwRange
r             ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      InterleavedMutual KwRange
r [Declaration]
ds     -> KwRange -> [Declaration] -> Declaration
InterleavedMutual KwRange
r     ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      LoneConstructor KwRange
r   [Declaration]
ds     -> KwRange -> [Declaration] -> Declaration
LoneConstructor KwRange
r       ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      Mutual KwRange
r            [Declaration]
ds     -> KwRange -> [Declaration] -> Declaration
Mutual KwRange
r                ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      Module Range
r Erased
er QName
n Telescope
tel   [Declaration]
ds     -> Range
-> Erased -> QName -> Telescope -> [Declaration] -> Declaration
Module Range
r Erased
er QName
n Telescope
tel       ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      Macro KwRange
r             [Declaration]
ds     -> KwRange -> [Declaration] -> Declaration
Macro KwRange
r                 ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      Opaque KwRange
r [Declaration]
ds                -> KwRange -> [Declaration] -> Declaration
Opaque KwRange
r                ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      Record Range
r Erased
er Name
n [RecordDirective]
dir [LamBinding]
tel Expr
t [Declaration]
ds -> Range
-> Erased
-> Name
-> [RecordDirective]
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
Record Range
r Erased
er Name
n [RecordDirective]
dir [LamBinding]
tel Expr
t ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      RecordDef Range
r Name
n [RecordDirective]
dir [LamBinding]
tel   [Declaration]
ds -> Range
-> Name
-> [RecordDirective]
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Name
n [RecordDirective]
dir [LamBinding]
tel   ([Declaration] -> Declaration) -> m [Declaration] -> m Declaration
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> [Declaration] -> m [Declaration]
preTraverseDecl Declaration -> m Declaration
f [Declaration]
ds
      TypeSig ArgInfo
_ TacticAttribute
_ Name
_ Expr
_            -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      FieldSig IsInstance
_ TacticAttribute
_ Name
_ Arg Expr
_           -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Generalize KwRange
_ [Declaration]
_             -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Field KwRange
_ [Declaration]
_                  -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca    -> (Declaration -> m Declaration) -> WhereClause -> m WhereClause
forall a (m :: * -> *).
(TraverseDecl a, Monad m) =>
(Declaration -> m Declaration) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Declaration -> m Declaration) -> WhereClause -> m WhereClause
preTraverseDecl Declaration -> m Declaration
f WhereClause
wh m WhereClause -> (WhereClause -> Declaration) -> m Declaration
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ WhereClause
wh' -> LHS -> RHS -> WhereClause -> Bool -> Declaration
FunClause LHS
lhs RHS
rhs WhereClause
wh' Bool
ca
      DataSig Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_          -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Data Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_ [Declaration]
_           -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      DataDef Range
_ Name
_ [LamBinding]
_ [Declaration]
_            -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      RecordSig Range
_ Erased
_ Name
_ [LamBinding]
_ Expr
_        -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Infix Fixity
_ List1 Name
_                  -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Syntax Name
_ Notation
_                 -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      PatternSyn Range
_ Name
_ [WithHiding Name]
_ Pattern
_         -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Postulate KwRange
_ [Declaration]
_              -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Primitive KwRange
_ [Declaration]
_              -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Open Range
_ QName
_ ImportDirective
_                 -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Import Range
_ QName
_ Maybe AsName
_ OpenShortHand
_ ImportDirective
_           -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      ModuleMacro Range
_ Erased
_ Name
_ ModuleApplication
_ OpenShortHand
_ ImportDirective
_    -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      UnquoteDecl Range
_ [Name]
_ Expr
_          -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      UnquoteDef Range
_ [Name]
_ Expr
_           -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      UnquoteData Range
_ Name
_ [Name]
_ Expr
_        -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Pragma Pragma
_                   -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d
      Unfolding KwRange
_ [QName]
_              -> Declaration -> m Declaration
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Declaration
d