{-# LANGUAGE CPP          #-}

-- | Tree traversal for internal syntax.

module Agda.Syntax.Internal.Generic where

#if __GLASGOW_HASKELL__ < 804
import Data.Monoid ((<>))
#endif
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Utils.Functor

-- | Generic term traversal.
--
--   Note: ignores sorts in terms!
--   (Does not traverse into or collect from them.)

class TermLike a where

  -- | Generic traversal with post-traversal action.
  --   Ignores sorts.
  traverseTermM :: Monad m => (Term -> m Term) -> a -> m a

  default traverseTermM :: (Monad m, Traversable f, TermLike b, f b ~ a)
                        => (Term -> m Term) -> a -> m a
  traverseTermM = 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 :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM

  -- | Generic fold, ignoring sorts.
  foldTerm :: Monoid m => (Term -> m) -> a -> m

  default foldTerm
    :: (Monoid m, Foldable f, TermLike b, f b ~ a) => (Term -> m) -> a -> m
  foldTerm = 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. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm

-- Constants

instance TermLike Bool where
  traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Bool -> m Bool
traverseTermM Term -> m Term
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  foldTerm :: forall m. Monoid m => (Term -> m) -> Bool -> m
foldTerm Term -> m
_      = forall a. Monoid a => a
mempty

instance TermLike Int where
  traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Int -> m Int
traverseTermM Term -> m Term
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  foldTerm :: forall m. Monoid m => (Term -> m) -> Int -> m
foldTerm Term -> m
_      = forall a. Monoid a => a
mempty

instance TermLike Integer where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Integer -> m Integer
traverseTermM Term -> m Term
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  foldTerm :: forall m. Monoid m => (Term -> m) -> Integer -> m
foldTerm Term -> m
_      = forall a. Monoid a => a
mempty

instance TermLike Char where
  traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Char -> m Char
traverseTermM Term -> m Term
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  foldTerm :: forall m. Monoid m => (Term -> m) -> Char -> m
foldTerm Term -> m
_      = forall a. Monoid a => a
mempty

instance TermLike QName where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> QName -> m QName
traverseTermM Term -> m Term
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure
  foldTerm :: forall m. Monoid m => (Term -> m) -> QName -> m
foldTerm Term -> m
_      = forall a. Monoid a => a
mempty

-- Functors

instance TermLike a => TermLike (Elim' a)      where
instance TermLike a => TermLike (Arg a)        where
instance TermLike a => TermLike (Dom a)        where
instance TermLike a => TermLike [a]            where
instance TermLike a => TermLike (Maybe a)      where
instance TermLike a => TermLike (Blocked a)    where
instance TermLike a => TermLike (Abs a)        where
instance TermLike a => TermLike (Tele a)       where
instance TermLike a => TermLike (WithHiding a) where

-- Tuples

instance (TermLike a, TermLike b) => TermLike (a, b) where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> (a, b) -> m (a, b)
traverseTermM Term -> m Term
f (a
x, b
y) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f b
y
  foldTerm :: forall m. Monoid m => (Term -> m) -> (a, b) -> m
foldTerm Term -> m
f (a
x, b
y) = forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f a
x forall a. Monoid a => a -> a -> a
`mappend` forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f b
y

instance (TermLike a, TermLike b, TermLike c) => TermLike (a, b, c) where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> (a, b, c) -> m (a, b, c)
traverseTermM Term -> m Term
f (a
x, b
y, c
z) = (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f c
z
  foldTerm :: forall m. Monoid m => (Term -> m) -> (a, b, c) -> m
foldTerm Term -> m
f (a
x, b
y, c
z) = forall a. Monoid a => [a] -> a
mconcat [forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f a
x, forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f b
y, forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f c
z]

instance (TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d) where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> (a, b, c, d) -> m (a, b, c, d)
traverseTermM Term -> m Term
f (a
x, b
y, c
z, d
u) = (,,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f a
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f b
y forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f c
z forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f d
u
  foldTerm :: forall m. Monoid m => (Term -> m) -> (a, b, c, d) -> m
foldTerm Term -> m
f (a
x, b
y, c
z, d
u) = forall a. Monoid a => [a] -> a
mconcat [forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f a
x, forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f b
y, forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f c
z, forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f d
u]

-- Real terms

instance TermLike Term where

  traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
traverseTermM Term -> m Term
f = \case
    Var Int
i Elims
xs    -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> Elims -> Term
Var Int
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Elims
xs
    Def QName
c Elims
xs    -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> Elims -> Term
Def QName
c forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Elims
xs
    Con ConHead
c ConInfo
ci Elims
xs -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Elims
xs
    Lam ArgInfo
h Abs Term
b     -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ArgInfo -> Abs Term -> Term
Lam ArgInfo
h forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Abs Term
b
    Pi Dom Type
a Abs Type
b      -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Dom Type -> Abs Type -> Term
Pi forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f (Dom Type
a, Abs Type
b)
    MetaV MetaId
m Elims
xs  -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< MetaId -> Elims -> Term
MetaV MetaId
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Elims
xs
    Level Level
l     -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Level -> Term
Level forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Level
l
    t :: Term
t@Lit{}     -> Term -> m Term
f Term
t
    Sort Sort
s      -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Sort -> Term
Sort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Sort
s
    DontCare Term
mv -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> Term
DontCare forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Term
mv
    Dummy String
s Elims
xs  -> Term -> m Term
f forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> Elims -> Term
Dummy String
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Elims
xs

  foldTerm :: forall m. Monoid m => (Term -> m) -> Term -> m
foldTerm Term -> m
f Term
t = Term -> m
f Term
t forall a. Monoid a => a -> a -> a
`mappend` case Term
t of
    Var Int
i Elims
xs    -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
xs
    Def QName
c Elims
xs    -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
xs
    Con ConHead
c ConInfo
ci Elims
xs -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
xs
    Lam ArgInfo
h Abs Term
b     -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Abs Term
b
    Pi Dom Type
a Abs Type
b      -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Dom Type
a, Abs Type
b)
    MetaV MetaId
m Elims
xs  -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
xs
    Level Level
l     -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Level
l
    Lit Literal
_       -> forall a. Monoid a => a
mempty
    Sort Sort
s      -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
s
    DontCare Term
mv -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Term
mv
    Dummy String
_ Elims
xs  -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
xs

instance TermLike Level where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Level -> m Level
traverseTermM Term -> m Term
f (Max Integer
n [PlusLevel' Term]
as) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f [PlusLevel' Term]
as
  foldTerm :: forall m. Monoid m => (Term -> m) -> Level -> m
foldTerm Term -> m
f      (Max Integer
n [PlusLevel' Term]
as) = forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f [PlusLevel' Term]
as

instance TermLike PlusLevel where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> PlusLevel' Term -> m (PlusLevel' Term)
traverseTermM Term -> m Term
f (Plus Integer
n Term
l) = forall t. Integer -> t -> PlusLevel' t
Plus Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Term
l
  foldTerm :: forall m. Monoid m => (Term -> m) -> PlusLevel' Term -> m
foldTerm Term -> m
f (Plus Integer
_ Term
l)      = forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Term
l

instance TermLike Type where
  traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Type -> m Type
traverseTermM Term -> m Term
f (El Sort
s Term
t) = forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Term
t
  foldTerm :: forall m. Monoid m => (Term -> m) -> Type -> m
foldTerm Term -> m
f (El Sort
s Term
t) = forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Term
t

instance TermLike Sort where
  traverseTermM :: forall (m :: * -> *). Monad m => (Term -> m Term) -> Sort -> m Sort
traverseTermM Term -> m Term
f = \case
    Type Level
l     -> forall t. Level' t -> Sort' t
Type forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Level
l
    Prop Level
l     -> forall t. Level' t -> Sort' t
Prop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Level
l
    s :: Sort
s@(Inf IsFibrant
_ Integer
_)-> forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    SSet Level
l     -> forall t. Level' t -> Sort' t
SSet forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Level
l
    s :: Sort
s@Sort
SizeUniv -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
LockUniv -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
IntervalUniv -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    PiSort Dom' Term Term
a Sort
b Abs Sort
c -> forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
PiSort   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Dom' Term Term
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Sort
b forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Abs Sort
c
    FunSort Sort
a Sort
b -> forall t. Sort' t -> Sort' t -> Sort' t
FunSort   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Sort
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Sort
b
    UnivSort Sort
a -> forall t. Sort' t -> Sort' t
UnivSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Sort
a
    MetaS MetaId
x Elims
es -> forall t. MetaId -> [Elim' t] -> Sort' t
MetaS MetaId
x  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Elims
es
    DefS QName
q Elims
es  -> forall t. QName -> [Elim' t] -> Sort' t
DefS QName
q   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Elims
es
    s :: Sort
s@(DummyS String
_) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s

  foldTerm :: forall m. Monoid m => (Term -> m) -> Sort -> m
foldTerm Term -> m
f = \case
    Type Level
l     -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Level
l
    Prop Level
l     -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Level
l
    Inf IsFibrant
_ Integer
_    -> forall a. Monoid a => a
mempty
    SSet Level
l     -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Level
l
    Sort
SizeUniv   -> forall a. Monoid a => a
mempty
    Sort
LockUniv   -> forall a. Monoid a => a
mempty
    Sort
IntervalUniv -> forall a. Monoid a => a
mempty
    PiSort Dom' Term Term
a Sort
b Abs Sort
c -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Dom' Term Term
a forall a. Semigroup a => a -> a -> a
<> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
b forall a. Semigroup a => a -> a -> a
<> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Abs Sort
c
    FunSort Sort
a Sort
b -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
a forall a. Semigroup a => a -> a -> a
<> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
b
    UnivSort Sort
a -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Sort
a
    MetaS MetaId
_ Elims
es -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
es
    DefS QName
_ Elims
es  -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
es
    DummyS String
_   -> forall a. Monoid a => a
mempty

instance TermLike EqualityView where

  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> EqualityView -> m EqualityView
traverseTermM Term -> m Term
f = \case
    OtherType Type
t -> Type -> EqualityView
OtherType
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Type
t
    IdiomType Type
t -> Type -> EqualityView
IdiomType
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Type
t
    EqualityType Sort
s QName
eq Args
l Arg Term
t Arg Term
a Arg Term
b -> Sort
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Sort
s QName
eq
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f) Args
l
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Arg Term
t
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Arg Term
a
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
f Arg Term
b

  foldTerm :: forall m. Monoid m => (Term -> m) -> EqualityView -> m
foldTerm Term -> m
f = \case
    OtherType Type
t -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
    IdiomType Type
t -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
    EqualityType Sort
s QName
eq Args
l Arg Term
t Arg Term
a Arg Term
b -> forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Args
l forall a. [a] -> [a] -> [a]
++ [Arg Term
t, Arg Term
a, Arg Term
b])

-- | Put it in a monad to make it possible to do strictly.
copyTerm :: (TermLike a, Monad m) => a -> m a
copyTerm :: forall a (m :: * -> *). (TermLike a, Monad m) => a -> m a
copyTerm = forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
traverseTermM forall (m :: * -> *) a. Monad m => a -> m a
return