-- | 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 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.
--
--   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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr

  default foldExpr
    :: (Monoid m, Foldable t, ExprLike b, t b ~ a)
    => (Expr -> m) -> a -> m
  foldExpr = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a 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 = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
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
_ ()
_   = forall a. Monoid a => a
mempty
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> () -> m ()
traverseExpr Expr -> m Expr
_ = forall (m :: * -> *) a. Monad m => a -> m a
return

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

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

instance ExprLike Bool where
  mapExpr :: (Expr -> Expr) -> Bool -> Bool
mapExpr Expr -> Expr
_      = forall a. a -> a
id
  foldExpr :: forall m. Monoid m => (Expr -> m) -> Bool -> m
foldExpr Expr -> m
_ Bool
_   = forall a. Monoid a => a
mempty
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> Bool -> m Bool
traverseExpr Expr -> m Expr
_ = 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 (WithHiding a)

instance ExprLike a => ExprLike (MaybePlaceholder a)
instance ExprLike a => ExprLike (RHS' 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      = forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f) (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 = forall (f :: * -> *) a c b d.
Functor f =>
(a -> f c) -> (b -> f d) -> Either a b -> f (Either c d)
traverseEither (forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f) (forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f)
  foldExpr :: forall m. Monoid m => (Expr -> m) -> Either a b -> m
foldExpr Expr -> m
f     = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f) (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) = (forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
x, 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) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
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) = forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f a
x forall a. Monoid a => a -> a -> a
`mappend` 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) = (forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
x, forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f b
y, 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) = (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
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) = forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f a
x forall a. Monoid a => a -> a -> a
`mappend` forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f b
y forall a. Monoid a => a -> a -> a
`mappend` 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) = (forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
x, forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f b
y, forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f c
z, 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) = (,,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f c
z forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
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) = forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f a
x forall a. Monoid a => a -> a -> a
`mappend` forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f b
y forall a. Monoid a => a -> a -> a
`mappend` forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f c
z forall a. Monoid a => a -> a -> a
`mappend` 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 forall a b. (a -> b) -> a -> b
$ Expr
e0
     Lit{}              -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     QuestionMark{}     -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     Underscore{}       -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     RawApp Range
r List2 Expr
es        -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> List2 Expr -> Expr
RawApp Range
r               forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE List2 Expr
es
     App Range
r Expr
e NamedArg Expr
es         -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Expr -> NamedArg Expr -> Expr
App Range
r       (forall e. ExprLike e => e -> e
mapE Expr
e)   forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE NamedArg Expr
es
     OpApp Range
r QName
q Set Name
ns OpAppArgs
es    -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> QName -> Set Name -> OpAppArgs -> Expr
OpApp Range
r QName
q Set Name
ns           forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE OpAppArgs
es
     WithApp Range
r Expr
e [Expr]
es     -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Expr -> [Expr] -> Expr
WithApp Range
r   (forall e. ExprLike e => e -> e
mapE Expr
e)   forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE [Expr]
es
     HiddenArg Range
r Named_ Expr
e      -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Named_ Expr -> Expr
HiddenArg Range
r            forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Named_ Expr
e
     InstanceArg Range
r Named_ Expr
e    -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Named_ Expr -> Expr
InstanceArg Range
r          forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Named_ Expr
e
     Lam Range
r List1 LamBinding
bs Expr
e         -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> List1 LamBinding -> Expr -> Expr
Lam Range
r       (forall e. ExprLike e => e -> e
mapE List1 LamBinding
bs)  forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
     AbsurdLam{}        -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     ExtendedLam Range
r Erased
e List1 LamClause
cs -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Erased -> List1 LamClause -> Expr
ExtendedLam Range
r Erased
e        forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE List1 LamClause
cs
     Fun Range
r Arg Expr
a Expr
b          -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Arg Expr -> Expr -> Expr
Fun Range
r     (forall e. ExprLike e => e -> e
mapE forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Expr
a) forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
b
     Pi Telescope1
tel Expr
e           -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Telescope1 -> Expr -> Expr
Pi          (forall e. ExprLike e => e -> e
mapE Telescope1
tel) forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
     Rec Range
r RecordAssignments
es           -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> RecordAssignments -> Expr
Rec Range
r                  forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE RecordAssignments
es
     RecUpdate Range
r Expr
e [FieldAssignment]
es   -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Expr -> [FieldAssignment] -> Expr
RecUpdate Range
r (forall e. ExprLike e => e -> e
mapE Expr
e)   forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE [FieldAssignment]
es
     Let Range
r List1 Declaration
ds Maybe Expr
e         -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> List1 Declaration -> Maybe Expr -> Expr
Let Range
r       (forall e. ExprLike e => e -> e
mapE List1 Declaration
ds)  forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Maybe Expr
e
     Paren Range
r Expr
e          -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
Paren Range
r                forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
     IdiomBrackets Range
r [Expr]
es -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> [Expr] -> Expr
IdiomBrackets Range
r        forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE [Expr]
es
     DoBlock Range
r List1 DoStmt
ss       -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> List1 DoStmt -> Expr
DoBlock Range
r              forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE List1 DoStmt
ss
     Absurd{}           -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     As Range
r Name
x Expr
e           -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Name -> Expr -> Expr
As Range
r Name
x                 forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
     Dot Range
r Expr
e            -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
Dot Range
r                  forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
     DoubleDot Range
r Expr
e      -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
DoubleDot Range
r            forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
     Tactic Range
r Expr
e         -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Expr
Tactic Range
r     (forall e. ExprLike e => e -> e
mapE Expr
e)
     Quote{}            -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     QuoteTerm{}        -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     Unquote{}          -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     DontCare Expr
e         -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr -> Expr
DontCare               forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
     Equal{}            -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     Ellipsis{}         -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr
e0
     Generalized Expr
e      -> Expr -> Expr
f forall a b. (a -> b) -> a -> b
$ Expr -> Expr
Generalized            forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE Expr
e
   where
     mapE :: ExprLike e => e -> e
     mapE :: forall e. ExprLike e => e -> e
mapE = forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f

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

instance ExprLike FieldAssignment where
  mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment
mapExpr      Expr -> Expr
f (FieldAssignment Name
x Expr
e) = forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x (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' -> forall a. Name -> a -> FieldAssignment' a
FieldAssignment Name
x Expr
e') forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f Expr
e
  foldExpr :: forall m. Monoid m => (Expr -> m) -> FieldAssignment -> m
foldExpr     Expr -> m
f (FieldAssignment Name
_ Expr
e) = 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 (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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
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) = 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 -> forall e. Range -> List1 LamBinding -> e -> OpApp e
SyntaxBindingLambda Range
r (forall e. ExprLike e => e -> e
mapE List1 LamBinding
bs) forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE a
e
     Ordinary                 a
e -> forall e. e -> OpApp e
Ordinary                        forall a b. (a -> b) -> a -> b
$ forall e. ExprLike e => e -> e
mapE a
e
   where
     mapE :: ExprLike e => e -> e
     mapE :: forall e. ExprLike e => e -> e
mapE = forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f
  foldExpr :: forall m. Monoid m => (Expr -> m) -> OpApp a -> m
foldExpr     = forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> OpApp a -> m (OpApp a)
traverseExpr = 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 -> forall a. a -> LamBinding' a
DomainFull 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 = 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     = forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> LamBinding -> m LamBinding
traverseExpr = 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 (forall e. ExprLike e => e -> e
mapE [RewriteEqn]
res) (forall e. ExprLike e => e -> e
mapE [WithExpr]
wes)
   where
     mapE :: ExprLike a => a -> a
     mapE :: forall e. ExprLike e => e -> e
mapE = forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f
  foldExpr :: forall m. Monoid m => (Expr -> m) -> LHS -> m
foldExpr     = forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *). Monad m => (Expr -> m Expr) -> LHS -> m LHS
traverseExpr = 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    -> forall qn nm p e. List1 (qn, e) -> RewriteEqn' qn nm p e
Rewrite (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 -> forall qn nm p e.
qn -> List1 (Named nm (p, e)) -> RewriteEqn' qn nm p e
Invert qn
qn (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a -> b) -> a -> b
$ forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f) List1 (Named nm (p, e))
pes)
  foldExpr :: forall m. Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m
foldExpr     = 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 = 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 (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     = forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> LamClause -> m LamClause
traverseExpr = 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 (forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f Expr
e) (forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f [LamClause]
cs)
  mapExpr Expr -> Expr
f (DoThen Expr
e)        = Expr -> DoStmt
DoThen (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 (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     = forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> DoStmt -> m DoStmt
traverseExpr = 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 (forall e. ExprLike e => e -> e
mapE Telescope
bs) forall a b. (a -> b) -> a -> b
$ 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 = forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f
  foldExpr :: forall m. Monoid m => (Expr -> m) -> ModuleApplication -> m
foldExpr     = forall a. HasCallStack => a
__IMPOSSIBLE__
  traverseExpr :: forall (m :: * -> *).
Monad m =>
(Expr -> m Expr) -> ModuleApplication -> m ModuleApplication
traverseExpr = forall a. HasCallStack => a
__IMPOSSIBLE__

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

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


{- Template

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

-}