    {-# 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 = (b -> m b) -> f b -> m (f b)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((b -> m b) -> f b -> m (f b))
    -> ((Term -> m Term) -> b -> m b)
    -> (Term -> m Term)
    -> f b
    -> m (f b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m Term) -> b -> m b
    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 = (b -> m) -> f b -> m
    forall (t :: * -> *) m a.
    (Foldable t, Monoid m) =>
    (a -> m) -> t a -> m
    foldMap ((b -> m) -> f b -> m)
    -> ((Term -> m) -> b -> m) -> (Term -> m) -> f b -> m
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Term -> m) -> b -> m
    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
    _ = Bool -> m Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      foldTerm :: forall m. Monoid m => (Term -> m) -> Bool -> m
    foldTerm Term -> m
    _      = Bool -> 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
    _ = Int -> m Int
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      foldTerm :: forall m. Monoid m => (Term -> m) -> Int -> m
    foldTerm Term -> m
    _      = Int -> 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
    _ = Integer -> m Integer
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      foldTerm :: forall m. Monoid m => (Term -> m) -> Integer -> m
    foldTerm Term -> m
    _      = Integer -> 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
    _ = Char -> m Char
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      foldTerm :: forall m. Monoid m => (Term -> m) -> Char -> m
    foldTerm Term -> m
    _      = Char -> 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
    _ = QName -> m QName
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      foldTerm :: forall m. Monoid m => (Term -> m) -> QName -> m
    foldTerm Term -> m
    _      = QName -> 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) = (,) (a -> b -> (a, b)) -> m a -> m (b -> (a, b))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    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
    <*> (Term -> m Term) -> b -> m 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) = (Term -> m) -> a -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f a
    x m -> m -> m
    forall a. Monoid a => a -> a -> a
    `mappend` (Term -> m) -> b -> m
    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) = (,,) (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
    <$> (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    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
    <*> (Term -> m Term) -> b -> m b
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    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
    <*> (Term -> m Term) -> c -> m c
    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) = [m] -> m
    forall a. Monoid a => [a] -> a
    mconcat [(Term -> m) -> a -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f a
    x, (Term -> m) -> b -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f b
    y, (Term -> m) -> c -> m
    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) = (,,,) (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
    <$> (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    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
    <*> (Term -> m Term) -> b -> m b
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    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
    <*> (Term -> m Term) -> c -> m c
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    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
    <*> (Term -> m Term) -> d -> m d
    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) = [m] -> m
    forall a. Monoid a => [a] -> a
    mconcat [(Term -> m) -> a -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f a
    x, (Term -> m) -> b -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f b
    y, (Term -> m) -> c -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f c
    z, (Term -> m) -> d -> m
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Int -> Elims -> Term
    Var Int
    i (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Elims -> m Elims
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< QName -> Elims -> Term
    Def QName
    c (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Elims -> m Elims
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    c ConInfo
    ci (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Elims -> m Elims
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ArgInfo -> Abs Term -> Term
    Lam ArgInfo
    h (Abs Term -> Term) -> m (Abs Term) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Abs Term -> m (Abs Term)
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< (Dom Type -> Abs Type -> Term) -> (Dom Type, Abs Type) -> Term
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Dom Type -> Abs Type -> Term
    Pi ((Dom Type, Abs Type) -> Term) -> m (Dom Type, Abs Type) -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< MetaId -> Elims -> Term
    MetaV MetaId
    m (Elims -> Term) -> m Elims -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Elims -> m Elims
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Level -> Term
    Level (Level -> Term) -> m Level -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Level -> m Level
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Sort -> Term
    Sort (Sort -> Term) -> m Sort -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Sort -> m Sort
    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 (Term -> m Term) -> m Term -> m Term
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< Term -> Term
    DontCare (Term -> Term) -> m Term -> m Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Term -> m Term
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Term
    mv
        t :: Term
    t@Dummy{}   -> Term -> m Term
    f Term
    t

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

    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) = Integer -> [PlusLevel' Term] -> Level
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    n ([PlusLevel' Term] -> Level) -> m [PlusLevel' Term] -> m Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> [PlusLevel' Term] -> m [PlusLevel' Term]
    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) = (Term -> m) -> [PlusLevel' Term] -> m
    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) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    n (Term -> PlusLevel' Term) -> m Term -> m (PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Term -> m Term
    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)      = (Term -> m) -> Term -> m
    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) = Sort -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort
    s (Term -> Type) -> m Term -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Term -> m Term
    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) = (Term -> m) -> Term -> m
    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     -> Level -> Sort
    forall t. Level' t -> Sort' t
    Type (Level -> Sort) -> m Level -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Level -> m Level
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Level
    l
        Prop Level
    l     -> Level -> Sort
    forall t. Level' t -> Sort' t
    Prop (Level -> Sort) -> m Level -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Level -> m Level
    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
    _)-> Sort -> m Sort
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
        SSet Level
    l     -> Level -> Sort
    forall t. Level' t -> Sort' t
    SSet (Level -> Sort) -> m Level -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Level -> m Level
    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 -> Sort -> m Sort
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
        s :: Sort
    s@Sort
    LockUniv -> Sort -> m Sort
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Sort
    s
        PiSort Dom' Term Term
    a Sort
    b Abs Sort
    c -> Dom' Term Term -> Sort -> Abs Sort -> Sort
    forall t. Dom' t t -> Sort' t -> Abs (Sort' t) -> Sort' t
    PiSort   (Dom' Term Term -> Sort -> Abs Sort -> Sort)
    -> m (Dom' Term Term) -> m (Sort -> Abs Sort -> Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Dom' Term Term -> m (Dom' Term Term)
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Dom' Term Term
    a m (Sort -> Abs Sort -> Sort) -> m Sort -> m (Abs Sort -> Sort)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> m Term) -> Sort -> m Sort
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Sort
    b m (Abs Sort -> Sort) -> m (Abs Sort) -> m Sort
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> m Term) -> Abs Sort -> m (Abs Sort)
    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 -> Sort -> Sort -> Sort
    forall t. Sort' t -> Sort' t -> Sort' t
    FunSort   (Sort -> Sort -> Sort) -> m Sort -> m (Sort -> Sort)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Sort -> m Sort
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Sort
    a m (Sort -> Sort) -> m Sort -> m Sort
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> m Term) -> Sort -> m Sort
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Sort
    b
        UnivSort Sort
    a -> Sort -> Sort
    forall t. Sort' t -> Sort' t
    UnivSort (Sort -> Sort) -> m Sort -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Sort -> m Sort
    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 -> MetaId -> Elims -> Sort
    forall t. MetaId -> [Elim' t] -> Sort' t
    MetaS MetaId
    x  (Elims -> Sort) -> m Elims -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Elims -> m Elims
    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  -> QName -> Elims -> Sort
    forall t. QName -> [Elim' t] -> Sort' t
    DefS QName
    q   (Elims -> Sort) -> m Elims -> m Sort
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Elims -> m Elims
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Elims
    es
        s :: Sort
    s@DummyS{} -> Sort -> m Sort
    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     -> (Term -> m) -> Level -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Level
    l
        Prop Level
    l     -> (Term -> m) -> Level -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Level
    l
        Inf IsFibrant
    _ Integer
    _    -> m
    forall a. Monoid a => a
    mempty
        SSet Level
    l     -> (Term -> m) -> Level -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Level
    l
        Sort
    SizeUniv   -> m
    forall a. Monoid a => a
    mempty
        Sort
    LockUniv   -> m
    forall a. Monoid a => a
    mempty
        PiSort Dom' Term Term
    a Sort
    b Abs Sort
    c -> (Term -> m) -> Dom' Term Term -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Dom' Term Term
    a m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Term -> m) -> Sort -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Sort
    b m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Term -> m) -> Abs Sort -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Abs Sort
    c
        FunSort Sort
    a Sort
    b -> (Term -> m) -> Sort -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Sort
    a m -> m -> m
    forall a. Semigroup a => a -> a -> a
    <> (Term -> m) -> Sort -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Sort
    b
        UnivSort Sort
    a -> (Term -> m) -> Sort -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Sort
    a
        MetaS MetaId
    _ Elims
    es -> (Term -> m) -> Elims -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Elims
    es
        DefS QName
    _ Elims
    es  -> (Term -> m) -> Elims -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Elims
    es
        DummyS{}   -> m
    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
          (Type -> EqualityView) -> m Type -> m EqualityView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Type -> m Type
    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
          (Type -> EqualityView) -> m Type -> m EqualityView
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Term -> m Term) -> Type -> m Type
    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 [Arg Term]
    l Arg Term
    t Arg Term
    a Arg Term
    b -> Sort
    -> QName
    -> [Arg Term]
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> EqualityView
    EqualityType Sort
    s QName
    eq
          ([Arg Term] -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
    -> m [Arg Term]
    -> m (Arg Term -> Arg Term -> Arg Term -> EqualityView)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Arg Term -> m (Arg Term)) -> [Arg Term] -> m [Arg Term]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse ((Term -> m Term) -> Arg Term -> m (Arg Term)
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f) [Arg Term]
    l
          m (Arg Term -> Arg Term -> Arg Term -> EqualityView)
    -> m (Arg Term) -> m (Arg Term -> Arg Term -> EqualityView)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> m Term) -> Arg Term -> m (Arg Term)
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Arg Term
    t
          m (Arg Term -> Arg Term -> EqualityView)
    -> m (Arg Term) -> m (Arg Term -> EqualityView)
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> m Term) -> Arg Term -> m (Arg Term)
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    f Arg Term
    a
          m (Arg Term -> EqualityView) -> m (Arg Term) -> m EqualityView
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Term -> m Term) -> Arg Term -> m (Arg Term)
    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 -> (Term -> m) -> Type -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Type
    t
        IdiomType Type
    t -> (Term -> m) -> Type -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f Type
    t
        EqualityType Sort
    s QName
    eq [Arg Term]
    l Arg Term
    t Arg Term
    a Arg Term
    b -> (Term -> m) -> [Arg Term] -> m
    forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
    foldTerm Term -> m
    f ([Arg Term]
    l [Arg Term] -> [Arg Term] -> [Arg Term]
    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 = (Term -> m Term) -> a -> m a
    forall a (m :: * -> *).
    (TermLike a, Monad m) =>
    (Term -> m Term) -> a -> m a
    traverseTermM Term -> m Term
    forall (m :: * -> *) a. Monad m => a -> m a
    return