{-# 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) -> a -> m a
(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)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> f a -> f (f b)
traverse ((b -> m b) -> a -> m a)
-> ((Term -> m Term) -> b -> m b) -> (Term -> m Term) -> a -> m a
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> b -> m b
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) -> a -> m
(b -> m) -> f b -> m
forall m a. Monoid m => (a -> m) -> f a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((b -> m) -> a -> m)
-> ((Term -> m) -> b -> m) -> (Term -> m) -> a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term -> m) -> b -> m
forall m. Monoid m => (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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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
forall (m :: * -> *). 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 a b. m (a -> b) -> m a -> m 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
forall (m :: * -> *). Monad m => (Term -> m Term) -> b -> m b
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 m. Monoid m => (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 m. Monoid m => (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
forall (m :: * -> *). 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 a b. m (a -> b) -> m a -> m 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
forall (m :: * -> *). Monad m => (Term -> m Term) -> b -> m b
traverseTermM Term -> m Term
f b
y m (c -> (a, b, c)) -> m c -> m (a, b, c)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> m Term) -> c -> m c
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> c -> m c
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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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
forall (m :: * -> *). 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 a b. m (a -> b) -> m a -> m 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
forall (m :: * -> *). Monad m => (Term -> m Term) -> b -> m b
traverseTermM Term -> m Term
f b
y m (c -> d -> (a, b, c, d)) -> m c -> m (d -> (a, b, c, d))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> m Term) -> c -> m c
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> c -> m c
traverseTermM Term -> m Term
f c
z m (d -> (a, b, c, d)) -> m d -> m (a, b, c, d)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> m Term) -> d -> m d
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> d -> m d
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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Elims -> m Elims
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Elims -> m Elims
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Elims -> m Elims
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Abs Term -> m (Abs Term)
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> (Dom Type, Abs Type) -> m (Dom Type, Abs Type)
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Elims -> m Elims
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Level -> m Level
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Sort -> m Sort
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
traverseTermM Term -> m Term
f Term
mv
    Dummy String
s 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
=<< String -> Elims -> Term
Dummy String
s (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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Elims -> m Elims
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 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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (Term -> m) -> Term -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Term
mv
    Dummy String
_ Elims
xs  -> (Term -> m) -> Elims -> m
forall m. Monoid m => (Term -> m) -> Elims -> m
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) = 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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> [PlusLevel' Term] -> m [PlusLevel' Term]
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 m. Monoid m => (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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
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 m. Monoid m => (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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Term -> m Term
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 m. Monoid m => (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
    Univ Univ
u Level
l   -> Univ -> Level -> Sort
forall t. Univ -> Level' t -> Sort' t
Univ Univ
u (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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Level -> m Level
traverseTermM Term -> m Term
f Level
l
    s :: Sort
s@(Inf Univ
_ Integer
_)-> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
SizeUniv -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
LockUniv -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
LevelUniv -> Sort -> m Sort
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Sort
s
    s :: Sort
s@Sort
IntervalUniv -> Sort -> m Sort
forall a. a -> m a
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Dom' Term Term -> m (Dom' Term Term)
traverseTermM Term -> m Term
f Dom' Term Term
a m (Sort -> Abs Sort -> Sort) -> m Sort -> m (Abs Sort -> Sort)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Sort -> m Sort
traverseTermM Term -> m Term
f Sort
b m (Abs Sort -> Sort) -> m (Abs Sort) -> m Sort
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Abs Sort -> m (Abs Sort)
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Sort -> m Sort
traverseTermM Term -> m Term
f Sort
a m (Sort -> Sort) -> m Sort -> m Sort
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Sort -> m Sort
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Sort -> m Sort
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Elims -> m Elims
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Elims -> m Elims
traverseTermM Term -> m Term
f Elims
es
    s :: Sort
s@(DummyS String
_) -> Sort -> m Sort
forall a. a -> m a
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
    Univ Univ
_ Level
l   -> (Term -> m) -> Level -> m
forall m. Monoid m => (Term -> m) -> Level -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Level
l
    Inf Univ
_ Integer
_    -> m
forall a. Monoid a => a
mempty
    Sort
SizeUniv   -> m
forall a. Monoid a => a
mempty
    Sort
LockUniv   -> m
forall a. Monoid a => a
mempty
    Sort
LevelUniv  -> m
forall a. Monoid a => a
mempty
    Sort
IntervalUniv -> m
forall a. Monoid a => a
mempty
    PiSort Dom' Term Term
a Sort
b Abs Sort
c -> (Term -> m) -> Dom' Term Term -> m
forall m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (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 m. Monoid m => (Term -> m) -> Elims -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Elims
es
    DummyS String
_   -> 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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Type -> m Type
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> Type -> m Type
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
      (Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> m Args -> 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)) -> Args -> m Args
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Term -> m Term) -> Arg Term -> m (Arg Term)
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
traverseTermM Term -> m Term
f) Args
l
      m (Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> m (Arg Term) -> m (Arg Term -> Arg Term -> EqualityView)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
traverseTermM Term -> m Term
f Arg Term
t
      m (Arg Term -> Arg Term -> EqualityView)
-> m (Arg Term) -> m (Arg Term -> EqualityView)
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
traverseTermM Term -> m Term
f Arg Term
a
      m (Arg Term -> EqualityView) -> m (Arg Term) -> m EqualityView
forall a b. m (a -> b) -> m a -> m b
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
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
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 m. Monoid m => (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 m. Monoid m => (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 Args
l Arg Term
t Arg Term
a Arg Term
b -> (Term -> m) -> Args -> m
forall m. Monoid m => (Term -> m) -> Args -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Args
l Args -> Args -> Args
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
forall (m :: * -> *). Monad m => (Term -> m Term) -> a -> m a
traverseTermM Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return