-- | 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.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'.

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

  foldExpr :: Monoid m => (Expr -> m) -> a -> m
  -- ^ This is a reduce.

  traverseExpr = (Expr -> m Expr) -> a -> m a
forall a. HasCallStack => a
__IMPOSSIBLE__  -- TODO: implement!
  foldExpr     = (Expr -> m) -> a -> m
forall a. HasCallStack => a
__IMPOSSIBLE__  -- TODO: implement!

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

instance ExprLike () where
  mapExpr :: (Expr -> Expr) -> () -> ()
mapExpr Expr -> Expr
f = () -> ()
forall a. a -> a
id

instance ExprLike Name where
  mapExpr :: (Expr -> Expr) -> Name -> Name
mapExpr Expr -> Expr
f = Name -> Name
forall a. a -> a
id

instance ExprLike QName where
  mapExpr :: (Expr -> Expr) -> QName -> QName
mapExpr Expr -> Expr
f = QName -> QName
forall a. a -> a
id

instance ExprLike Bool where
  mapExpr :: (Expr -> Expr) -> Bool -> Bool
mapExpr Expr -> Expr
f = Bool -> Bool
forall a. a -> a
id

-- * Instances for functors.

instance ExprLike a => ExprLike (WithHiding a) where
  mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a
mapExpr      = (a -> a) -> WithHiding a -> WithHiding a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> WithHiding a -> WithHiding a)
-> ((Expr -> Expr) -> a -> a)
-> (Expr -> Expr)
-> WithHiding a
-> WithHiding a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> WithHiding a -> m (WithHiding a)
traverseExpr = (a -> m a) -> WithHiding a -> m (WithHiding a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> WithHiding a -> m (WithHiding a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> WithHiding a
-> m (WithHiding a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> WithHiding a -> m
foldExpr     = (a -> m) -> WithHiding a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> WithHiding a -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> WithHiding a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

instance ExprLike a => ExprLike (Named name a) where
  mapExpr :: (Expr -> Expr) -> Named name a -> Named name a
mapExpr      = (a -> a) -> Named name a -> Named name a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> Named name a -> Named name a)
-> ((Expr -> Expr) -> a -> a)
-> (Expr -> Expr)
-> Named name a
-> Named name a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> Named name a -> m (Named name a)
traverseExpr = (a -> m a) -> Named name a -> m (Named name a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> Named name a -> m (Named name a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> Named name a
-> m (Named name a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> Named name a -> m
foldExpr     = (a -> m) -> Named name a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> Named name a -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> Named name a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

instance ExprLike a => ExprLike (Arg a) where  -- TODO guilhem
  mapExpr :: (Expr -> Expr) -> Arg a -> Arg a
mapExpr      = (a -> a) -> Arg a -> Arg a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> Arg a -> Arg a)
-> ((Expr -> Expr) -> a -> a) -> (Expr -> Expr) -> Arg a -> Arg a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> Arg a -> m (Arg a)
traverseExpr = (a -> m a) -> Arg a -> m (Arg a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> Arg a -> m (Arg a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> Arg a
-> m (Arg a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> Arg a -> m
foldExpr     = (a -> m) -> Arg a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> Arg a -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> Arg a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

instance ExprLike a => ExprLike [a] where
  mapExpr :: (Expr -> Expr) -> [a] -> [a]
mapExpr      = (a -> a) -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> [a] -> [a])
-> ((Expr -> Expr) -> a -> a) -> (Expr -> Expr) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> [a] -> m [a]
traverseExpr = (a -> m a) -> [a] -> m [a]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> [a] -> m [a])
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> [a]
-> m [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> [a] -> m
foldExpr     = (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> [a] -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> [a] -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

instance ExprLike a => ExprLike (Maybe a) where
  mapExpr :: (Expr -> Expr) -> Maybe a -> Maybe a
mapExpr      = (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> Maybe a -> Maybe a)
-> ((Expr -> Expr) -> a -> a)
-> (Expr -> Expr)
-> Maybe a
-> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> Maybe a -> m (Maybe a)
traverseExpr = (a -> m a) -> Maybe a -> m (Maybe a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> Maybe a -> m (Maybe a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> Maybe a
-> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> Maybe a -> m
foldExpr     = (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> Maybe a -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> Maybe a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

instance ExprLike a => ExprLike (MaybePlaceholder a) where
  mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a
mapExpr      = (a -> a) -> MaybePlaceholder a -> MaybePlaceholder a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> MaybePlaceholder a -> MaybePlaceholder a)
-> ((Expr -> Expr) -> a -> a)
-> (Expr -> Expr)
-> MaybePlaceholder a
-> MaybePlaceholder a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a)
traverseExpr = (a -> m a) -> MaybePlaceholder a -> m (MaybePlaceholder a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> MaybePlaceholder a -> m (MaybePlaceholder a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> MaybePlaceholder a
-> m (MaybePlaceholder a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> MaybePlaceholder a -> m
foldExpr     = (a -> m) -> MaybePlaceholder a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> MaybePlaceholder a -> m)
-> ((Expr -> m) -> a -> m)
-> (Expr -> m)
-> MaybePlaceholder a
-> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

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 (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 :: (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
traverseExpr Expr -> m Expr
f) ((Expr -> m Expr) -> b -> m b
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr Expr -> m Expr
f)
  foldExpr :: (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 a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f) ((Expr -> m) -> b -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr Expr -> m
f)

instance ExprLike a => ExprLike (TypedBinding' a) where
  mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a
mapExpr      = (a -> a) -> TypedBinding' a -> TypedBinding' a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> TypedBinding' a -> TypedBinding' a)
-> ((Expr -> Expr) -> a -> a)
-> (Expr -> Expr)
-> TypedBinding' a
-> TypedBinding' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a)
traverseExpr = (a -> m a) -> TypedBinding' a -> m (TypedBinding' a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> TypedBinding' a -> m (TypedBinding' a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> TypedBinding' a
-> m (TypedBinding' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> TypedBinding' a -> m
foldExpr     = (a -> m) -> TypedBinding' a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> TypedBinding' a -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> TypedBinding' a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

instance ExprLike a => ExprLike (RHS' a) where
  mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a
mapExpr      = (a -> a) -> RHS' a -> RHS' a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> RHS' a -> RHS' a)
-> ((Expr -> Expr) -> a -> a) -> (Expr -> Expr) -> RHS' a -> RHS' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> RHS' a -> m (RHS' a)
traverseExpr = (a -> m a) -> RHS' a -> m (RHS' a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> RHS' a -> m (RHS' a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> RHS' a
-> m (RHS' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> RHS' a -> m
foldExpr     = (a -> m) -> RHS' a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> RHS' a -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> RHS' a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

instance ExprLike a => ExprLike (WhereClause' a) where
  mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a
mapExpr      = (a -> a) -> WhereClause' a -> WhereClause' a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap     ((a -> a) -> WhereClause' a -> WhereClause' a)
-> ((Expr -> Expr) -> a -> a)
-> (Expr -> Expr)
-> WhereClause' a
-> WhereClause' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr
  traverseExpr :: (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a)
traverseExpr = (a -> m a) -> WhereClause' a -> m (WhereClause' a)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ((a -> m a) -> WhereClause' a -> m (WhereClause' a))
-> ((Expr -> m Expr) -> a -> m a)
-> (Expr -> m Expr)
-> WhereClause' a
-> m (WhereClause' a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m Expr) -> a -> m a
forall a (m :: * -> *).
(ExprLike a, Monad m) =>
(Expr -> m Expr) -> a -> m a
traverseExpr
  foldExpr :: (Expr -> m) -> WhereClause' a -> m
foldExpr     = (a -> m) -> WhereClause' a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap  ((a -> m) -> WhereClause' a -> m)
-> ((Expr -> m) -> a -> m) -> (Expr -> m) -> WhereClause' a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> m) -> a -> m
forall a m. (ExprLike a, Monoid m) => (Expr -> m) -> a -> m
foldExpr

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 :: (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
traverseExpr Expr -> m Expr
f a
x m (b -> (a, b)) -> m b -> m (a, 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
traverseExpr Expr -> m Expr
f b
y
  foldExpr :: (Expr -> m) -> (a, b) -> m
foldExpr     Expr -> m
f (a
x, b
y) = (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 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 :: (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
traverseExpr Expr -> m Expr
f a
x m (b -> c -> (a, b, c)) -> m b -> m (c -> (a, b, c))
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
traverseExpr Expr -> m Expr
f b
y m (c -> (a, b, c)) -> m c -> m (a, b, c)
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
traverseExpr Expr -> m Expr
f c
z
  foldExpr :: (Expr -> m) -> (a, b, c) -> m
foldExpr     Expr -> m
f (a
x, b
y, c
z) = (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 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 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 :: (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
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 (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
traverseExpr Expr -> m Expr
f b
y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
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
traverseExpr Expr -> m Expr
f c
z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
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
traverseExpr Expr -> m Expr
f d
w
  foldExpr :: (Expr -> m) -> (a, b, c, d) -> m
foldExpr     Expr -> m
f (a
x, b
y, c
z, d
w) = (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 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 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 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 [Expr]
es        -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> [Expr] -> Expr
RawApp Range
r               ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> [Expr]
forall a. ExprLike a => a -> a
mapE [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 a. ExprLike a => a -> a
mapE Expr
e)   (NamedArg Expr -> Expr) -> NamedArg Expr -> Expr
forall a b. (a -> b) -> a -> b
$ NamedArg Expr -> NamedArg Expr
forall a. ExprLike a => a -> a
mapE NamedArg Expr
es
     OpApp Range
r QName
q Set Name
ns [NamedArg (MaybePlaceholder (OpApp Expr))]
es    -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range
-> QName
-> Set Name
-> [NamedArg (MaybePlaceholder (OpApp Expr))]
-> Expr
OpApp Range
r QName
q Set Name
ns           ([NamedArg (MaybePlaceholder (OpApp Expr))] -> Expr)
-> [NamedArg (MaybePlaceholder (OpApp Expr))] -> Expr
forall a b. (a -> b) -> a -> b
$ [NamedArg (MaybePlaceholder (OpApp Expr))]
-> [NamedArg (MaybePlaceholder (OpApp Expr))]
forall a. ExprLike a => a -> a
mapE [NamedArg (MaybePlaceholder (OpApp Expr))]
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 a. ExprLike a => a -> a
mapE Expr
e)   ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> [Expr]
forall a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE Named_ Expr
e
     Lam Range
r [LamBinding]
bs Expr
e         -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> [LamBinding] -> Expr -> Expr
Lam Range
r       ([LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
mapE [LamBinding]
bs)  (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e
     AbsurdLam{}        -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     ExtendedLam Range
r [LamClause]
cs   -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> [LamClause] -> Expr
ExtendedLam Range
r          ([LamClause] -> Expr) -> [LamClause] -> Expr
forall a b. (a -> b) -> a -> b
$ [LamClause] -> [LamClause]
forall a. ExprLike a => a -> a
mapE [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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE Expr
b
     Pi Telescope
tel Expr
e           -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr -> Expr
Pi          (Telescope -> Telescope
forall a. ExprLike a => a -> a
mapE Telescope
tel) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e
     Set{}              -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     Prop{}             -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     SetN{}             -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     PropN{}            -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Expr
e0
     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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE Expr
e)   ([FieldAssignment] -> Expr) -> [FieldAssignment] -> Expr
forall a b. (a -> b) -> a -> b
$ [FieldAssignment] -> [FieldAssignment]
forall a. ExprLike a => a -> a
mapE [FieldAssignment]
es
     Let Range
r [Declaration]
ds Maybe Expr
e         -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> [Declaration] -> Maybe Expr -> Expr
Let Range
r       ([Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds)  (Maybe Expr -> Expr) -> Maybe Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Maybe Expr -> Maybe Expr
forall a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE [Expr]
es
     DoBlock Range
r [DoStmt]
ss       -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Range -> [DoStmt] -> Expr
DoBlock Range
r              ([DoStmt] -> Expr) -> [DoStmt] -> Expr
forall a b. (a -> b) -> a -> b
$ [DoStmt] -> [DoStmt]
forall a. ExprLike a => a -> a
mapE [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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE Expr
e
     ETel Telescope
tel           -> Expr -> Expr
f (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Expr
ETel                   (Telescope -> Expr) -> Telescope -> Expr
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope
forall a. ExprLike a => a -> a
mapE Telescope
tel
     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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE Expr
e
   where mapE :: a -> a
mapE a
e = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
e

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 :: (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
traverseExpr Expr -> m Expr
f Expr
e
  foldExpr :: (Expr -> m) -> FieldAssignment -> m
foldExpr     Expr -> m
f (FieldAssignment Name
_ Expr
e) = (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 :: (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
traverseExpr Expr -> m Expr
f [Expr]
es
  foldExpr :: (Expr -> m) -> ModuleAssignment -> m
foldExpr     Expr -> m
f (ModuleAssignment QName
m [Expr]
es ImportDirective
i) = (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 OpApp a
e0 = case OpApp a
e0 of
     SyntaxBindingLambda Range
r [LamBinding]
bs a
e -> Range -> [LamBinding] -> a -> OpApp a
forall e. Range -> [LamBinding] -> e -> OpApp e
SyntaxBindingLambda Range
r ([LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
mapE [LamBinding]
bs) (a -> OpApp a) -> a -> OpApp a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE a
e
   where mapE :: a -> a
mapE a
e = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
e

instance ExprLike LamBinding where
  mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding
mapExpr Expr -> Expr
f LamBinding
e0 = case LamBinding
e0 of
     DomainFree{}  -> LamBinding
e0
     DomainFull TypedBinding
bs -> TypedBinding -> LamBinding
forall a. a -> LamBinding' a
DomainFull (TypedBinding -> LamBinding) -> TypedBinding -> LamBinding
forall a b. (a -> b) -> a -> b
$ TypedBinding -> TypedBinding
forall a. ExprLike a => a -> a
mapE TypedBinding
bs
   where mapE :: a -> a
mapE a
e = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
e

instance ExprLike LHS where
  mapExpr :: (Expr -> Expr) -> LHS -> LHS
mapExpr Expr -> Expr
f LHS
e0 = case LHS
e0 of
     LHS Pattern
ps [RewriteEqn]
res [WithHiding Expr]
wes ExpandedEllipsis
ell -> Pattern
-> [RewriteEqn] -> [WithHiding Expr] -> ExpandedEllipsis -> LHS
LHS Pattern
ps ([RewriteEqn] -> [RewriteEqn]
forall a. ExprLike a => a -> a
mapE [RewriteEqn]
res) ([WithHiding Expr] -> [WithHiding Expr]
forall a. ExprLike a => a -> a
mapE [WithHiding Expr]
wes) ExpandedEllipsis
ell
   where mapE :: a -> a
mapE a
e = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
e

instance (ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn p e) where
  mapExpr :: (Expr -> Expr) -> RewriteEqn' qn p e -> RewriteEqn' qn p e
mapExpr Expr -> Expr
f = \case
    Rewrite [(qn, e)]
es    -> [(qn, e)] -> RewriteEqn' qn p e
forall qn p e. [(qn, e)] -> RewriteEqn' qn p e
Rewrite ((Expr -> Expr) -> [(qn, e)] -> [(qn, e)]
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f [(qn, e)]
es)
    Invert qn
qn [(p, e)]
pes -> qn -> [(p, e)] -> RewriteEqn' qn p e
forall qn p e. qn -> [(p, e)] -> RewriteEqn' qn p e
Invert qn
qn (((p, e) -> (p, e)) -> [(p, e)] -> [(p, e)]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Expr) -> e -> e
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f (e -> e) -> (p, e) -> (p, e)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) [(p, e)]
pes)

instance ExprLike LamClause where
  mapExpr :: (Expr -> Expr) -> LamClause -> LamClause
mapExpr Expr -> Expr
f (LamClause LHS
lhs RHS
rhs WhereClause
wh Bool
ca) =
    LHS -> RHS -> WhereClause -> Bool -> LamClause
LamClause ((Expr -> Expr) -> LHS -> LHS
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f LHS
lhs) ((Expr -> Expr) -> RHS -> RHS
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f RHS
rhs) ((Expr -> Expr) -> WhereClause -> WhereClause
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f WhereClause
wh) ((Expr -> Expr) -> Bool -> Bool
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f Bool
ca)

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 [Declaration]
ds)      = Range -> [Declaration] -> DoStmt
DoLet Range
r ((Expr -> Expr) -> [Declaration] -> [Declaration]
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f [Declaration]
ds)

instance ExprLike ModuleApplication where
  mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication
mapExpr Expr -> Expr
f ModuleApplication
e0 = case ModuleApplication
e0 of
     SectionApp Range
r Telescope
bs Expr
e -> Range -> Telescope -> Expr -> ModuleApplication
SectionApp Range
r (Telescope -> Telescope
forall a. ExprLike a => a -> a
mapE Telescope
bs) (Expr -> ModuleApplication) -> Expr -> ModuleApplication
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e
     RecordModuleInstance{} -> ModuleApplication
e0
   where mapE :: a -> a
mapE a
e = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
e

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 (Maybe Expr -> Maybe Expr
forall a. ExprLike a => a -> a
mapE Maybe Expr
t) Name
x (Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e)
     FieldSig IsInstance
i Maybe Expr
t Name
n Arg Expr
e          -> IsInstance -> Maybe Expr -> Name -> Arg Expr -> Declaration
FieldSig IsInstance
i (Maybe Expr -> Maybe Expr
forall a. ExprLike a => a -> a
mapE Maybe Expr
t) Name
n (Arg Expr -> Arg Expr
forall a. ExprLike a => a -> a
mapE Arg Expr
e)
     Field Range
r [Declaration]
fs                -> Range -> [Declaration] -> Declaration
Field Range
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 a. ExprLike a => a -> a
mapE LHS
lhs) (RHS -> RHS
forall a. ExprLike a => a -> a
mapE RHS
rhs) (WhereClause -> WhereClause
forall a. ExprLike a => a -> a
mapE WhereClause
wh) (Bool -> Bool
forall a. ExprLike a => a -> a
mapE Bool
ca)
     DataSig Range
r Name
x [LamBinding]
bs Expr
e          -> Range -> Name -> [LamBinding] -> Expr -> Declaration
DataSig Range
r Name
x ([LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
mapE [LamBinding]
bs)                (Expr -> Declaration) -> Expr -> Declaration
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
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 a. ExprLike a => a -> a
mapE [LamBinding]
bs)                ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
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 ([LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
mapE [LamBinding]
bs) (Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e)          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
cs
     RecordSig Range
r Name
ind [LamBinding]
bs Expr
e      -> Range -> Name -> [LamBinding] -> Expr -> Declaration
RecordSig Range
r Name
ind ([LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
mapE [LamBinding]
bs)            (Expr -> Declaration) -> Expr -> Declaration
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e
     RecordDef Range
r Name
n Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
c [LamBinding]
tel [Declaration]
ds -> Range
-> Name
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> [Declaration]
-> Declaration
RecordDef Range
r Name
n Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
c ([LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
mapE [LamBinding]
tel) ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     Record Range
r Name
n Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
c [LamBinding]
tel Expr
e [Declaration]
ds  -> Range
-> Name
-> Maybe (Ranged Induction)
-> Maybe HasEta
-> Maybe (Name, IsInstance)
-> [LamBinding]
-> Expr
-> [Declaration]
-> Declaration
Record Range
r Name
n Maybe (Ranged Induction)
ind Maybe HasEta
eta Maybe (Name, IsInstance)
c ([LamBinding] -> [LamBinding]
forall a. ExprLike a => a -> a
mapE [LamBinding]
tel) (Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e) ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     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                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     Abstract  Range
r [Declaration]
ds            -> Range -> [Declaration] -> Declaration
Abstract  Range
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     Private   Range
r Origin
o [Declaration]
ds          -> Range -> Origin -> [Declaration] -> Declaration
Private   Range
r Origin
o                        ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     InstanceB Range
r [Declaration]
ds            -> Range -> [Declaration] -> Declaration
InstanceB Range
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     Macro     Range
r [Declaration]
ds            -> Range -> [Declaration] -> Declaration
Macro     Range
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     Postulate Range
r [Declaration]
ds            -> Range -> [Declaration] -> Declaration
Postulate Range
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     Primitive Range
r [Declaration]
ds            -> Range -> [Declaration] -> Declaration
Primitive Range
r                          ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     Generalize Range
r [Declaration]
ds           -> Range -> [Declaration] -> Declaration
Generalize Range
r                         ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
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 (ModuleApplication -> ModuleApplication
forall a. ExprLike a => a -> a
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 (Telescope -> Telescope
forall a. ExprLike a => a -> a
mapE Telescope
tel)                ([Declaration] -> Declaration) -> [Declaration] -> Declaration
forall a b. (a -> b) -> a -> b
$ [Declaration] -> [Declaration]
forall a. ExprLike a => a -> a
mapE [Declaration]
ds
     UnquoteDecl Range
r [Name]
x Expr
e         -> Range -> [Name] -> Expr -> Declaration
UnquoteDecl Range
r [Name]
x (Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e)
     UnquoteDef Range
r [Name]
x Expr
e          -> Range -> [Name] -> Expr -> Declaration
UnquoteDef Range
r [Name]
x (Expr -> Expr
forall a. ExprLike a => a -> a
mapE Expr
e)
     e :: Declaration
e@Pragma{}                -> Declaration
e
   where mapE :: a -> a
mapE a
e = (Expr -> Expr) -> a -> a
forall a. ExprLike a => (Expr -> Expr) -> a -> a
mapExpr Expr -> Expr
f a
e

{- Template

instance ExprLike a where
  mapExpr f e0 = case e0 of
   where mapE e = mapExpr f e
-}