{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE Safe #-}

-- |
-- Module      : Data.Tree.ITree
-- Description : Type trees and indexed trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Definition of the trees used at the type level for the type safe BST and AVL trees.
module Data.Tree.ITree
  ( Tree (EmptyTree, ForkTree),
    ITree (EmptyITree, ForkITree),
  )
where

import Data.Kind (Type)
import Data.Tree.Node (Node)
import Prelude (Show (show), String, (++))

-- | Tree definition for the type level. Type safe trees are indexed by
-- type trees of the kind `'Tree`.
data Tree :: Type where
  EmptyTree :: Tree
  ForkTree :: Tree -> n -> Tree -> Tree

-- | Value level trees indexed by trees of kind `'Tree`.
-- The tree structure from the value level is replicated at the type level.
data ITree :: Tree -> Type where
  EmptyITree :: ITree 'EmptyTree
  ForkITree :: Show a => ITree l -> Node n a -> ITree r -> ITree ('ForkTree l (Node n a) r)

-- | `Show` instance for `ITree`.
instance Show (ITree t) where
  show :: ITree t -> String
show ITree t
EmptyITree = String
"E"
  show (ForkITree ITree l
l Node n a
n ITree r
r) = String
"F " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ITree l -> String
forall (t :: Tree). ITree t -> String
go ITree l
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node n a -> String
forall a. Show a => a -> String
show Node n a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ITree r -> String
forall (t :: Tree). ITree t -> String
go ITree r
r
    where
      go :: ITree t' -> String
      go :: forall (t :: Tree). ITree t -> String
go ITree t'
EmptyITree = String
"E"
      go (ForkITree ITree l
l' Node n a
n' ITree r
r') = String
"(F " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ITree l -> String
forall (t :: Tree). ITree t -> String
go ITree l
l' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Node n a -> String
forall a. Show a => a -> String
show Node n a
n' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ITree r -> String
forall (t :: Tree). ITree t -> String
go ITree r
r' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"