    {-# LANGUAGE CPP          #-}
    {-# LANGUAGE TypeFamilies #-}

    -- | Tree traversal for internal syntax.

    module Agda.Syntax.Internal.Generic where

    import Data.Traversable
    import Data.Monoid
    import Data.Foldable
    import Agda.Syntax.Common
    import Agda.Syntax.Internal

    -- | 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 = traverse . 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 = foldMap . foldTerm

    -- Constants

    instance TermLike Bool where
      traverseTermM _ = pure
      foldTerm _      = mempty

    instance TermLike Int where
      traverseTermM _ = pure
      foldTerm _      = mempty

    instance TermLike Integer where
      traverseTermM _ = pure
      foldTerm _      = mempty

    instance TermLike Char where
      traverseTermM _ = pure
      foldTerm _      = mempty

    instance TermLike QName where
      traverseTermM _ = pure
      foldTerm _      = 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 (Abs a)     where
    instance TermLike a => TermLike (Blocked a) where
    instance TermLike a => TermLike (Tele a)    where

    -- Tuples

    instance (TermLike a, TermLike b) => TermLike (a, b) where
      traverseTermM f (x, y) = (,) <$> traverseTermM f x <*> traverseTermM f y
      foldTerm f (x, y) = foldTerm f x `mappend` foldTerm f y

    instance (TermLike a, TermLike b, TermLike c) => TermLike (a, b, c) where
      traverseTermM f (x, y, z) = (,,) <$> traverseTermM f x <*> traverseTermM f y <*> traverseTermM f z
      foldTerm f (x, y, z) = mconcat [foldTerm f x, foldTerm f y, foldTerm f z]

    instance (TermLike a, TermLike b, TermLike c, TermLike d) => TermLike (a, b, c, d) where
      traverseTermM f (x, y, z, u) = (,,,) <$> traverseTermM f x <*> traverseTermM f y <*> traverseTermM f z <*> traverseTermM f u
      foldTerm f (x, y, z, u) = mconcat [foldTerm f x, foldTerm f y, foldTerm f z, foldTerm f u]

    -- Real terms

    instance TermLike Term where

      traverseTermM f t = case t of
        Var i xs    -> f =<< Var i <$> traverseTermM f xs
        Def c xs    -> f =<< Def c <$> traverseTermM f xs
        Con c ci xs -> f =<< Con c ci <$> traverseTermM f xs
        Lam h b     -> f =<< Lam h <$> traverseTermM f b
        Pi a b      -> f =<< uncurry Pi <$> traverseTermM f (a, b)
        MetaV m xs  -> f =<< MetaV m <$> traverseTermM f xs
        Level l     -> f =<< Level <$> traverseTermM f l
        Lit _       -> f t
        Sort s      -> f =<< Sort <$> traverseTermM f s
        DontCare mv -> f =<< DontCare <$> traverseTermM f mv
        Dummy{}     -> f t

      foldTerm f t = f t `mappend` case t of
        Var i xs    -> foldTerm f xs
        Def c xs    -> foldTerm f xs
        Con c ci xs -> foldTerm f xs
        Lam h b     -> foldTerm f b
        Pi a b      -> foldTerm f (a, b)
        MetaV m xs  -> foldTerm f xs
        Level l     -> foldTerm f l
        Lit _       -> mempty
        Sort s      -> foldTerm f s
        DontCare mv -> foldTerm f mv
        Dummy{}     -> mempty

    instance TermLike Level where
      traverseTermM f (Max as) = Max <$> traverseTermM f as
      foldTerm f      (Max as) = foldTerm f as

    instance TermLike PlusLevel where
      traverseTermM f l = case l of
        ClosedLevel{} -> return l
        Plus n l      -> Plus n <$> traverseTermM f l
      foldTerm f ClosedLevel{} = mempty
      foldTerm f (Plus _ l)    = foldTerm f l

    instance TermLike LevelAtom where
      traverseTermM f l = case l of
        MetaLevel m vs   -> MetaLevel m <$> traverseTermM f vs
        NeutralLevel r v -> NeutralLevel r <$> traverseTermM f v
        BlockedLevel m v -> BlockedLevel m <$> traverseTermM f v
        UnreducedLevel v -> UnreducedLevel <$> traverseTermM f v
      foldTerm f l = case l of
        MetaLevel m vs   -> foldTerm f vs
        NeutralLevel _ v -> foldTerm f v
        BlockedLevel _ v -> foldTerm f v
        UnreducedLevel v -> foldTerm f v

    instance TermLike Type where
      traverseTermM f (El s t) = El s <$> traverseTermM f t
      foldTerm f (El s t) = foldTerm f t

    instance TermLike Sort where
      traverseTermM f s = case s of
        Type l     -> Type <$> traverseTermM f l
        Prop l     -> Prop <$> traverseTermM f l
        Inf        -> pure s
        SizeUniv   -> pure s
        PiSort a b -> PiSort   <$> traverseTermM f a <*> traverseTermM f b
        UnivSort a -> UnivSort <$> traverseTermM f a
        MetaS x es -> MetaS x  <$> traverseTermM f es
        DefS q es  -> DefS q   <$> traverseTermM f es
        DummyS{}   -> pure s

      foldTerm f s = case s of
        Type l     -> foldTerm f l
        Prop l     -> foldTerm f l
        Inf        -> mempty
        SizeUniv   -> mempty
        PiSort a b -> foldTerm f a <> foldTerm f b
        UnivSort a -> foldTerm f a
        MetaS _ es -> foldTerm f es
        DefS _ es  -> foldTerm f es
        DummyS{}   -> mempty

    instance TermLike EqualityView where

      traverseTermM f v = case v of
        OtherType t -> OtherType
          <$> traverseTermM f t
        EqualityType s eq l t a b -> EqualityType s eq
          <$> traverse (traverseTermM f) l
          <*> traverseTermM f t
          <*> traverseTermM f a
          <*> traverseTermM f b

      foldTerm f v = case v of
        OtherType t -> foldTerm f t
        EqualityType s eq l t a b -> foldTerm f (l ++ [t, a, b])

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