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

-- |
-- Module      : Data.Tree.BST.Intern.Constructor
-- Description : Constructor of type safe internalist BST trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the constructor of type safe internalist BST
-- trees and instance definition for the `Show` type class.
module Data.Tree.BST.Intern.Constructors
  ( BST (EmptyBST, ForkBST),
  )
where

import Data.Kind (Type)
import Data.Tree.BST.Invariants (GtN, LtN)
import Data.Tree.ITree (Tree (EmptyTree, ForkTree))
import Data.Tree.Node (Node)
import Prelude
  ( Bool (True),
    Show (show),
    String,
    (++),
  )

-- | Constructor of internalist `BST` trees.
-- Given two `BST` trees and an arbitrary node, it tests at compile time wether the key
-- of the node verifies the `LtN` and `GtN` invariants with respect to each tree.
-- Notice that this is all that's needed to assert that the new tree is a `BST`,
-- since, by recursive logic, both left and right `BST` trees already respect the key ordering.
data BST :: Tree -> Type where
  EmptyBST :: BST 'EmptyTree
  ForkBST ::
    (Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
    BST l ->
    Node n a ->
    BST r ->
    BST ('ForkTree l (Node n a) r)

-- | Instance definition for the `Show` type class.
instance Show (BST t) where
  show :: BST t -> String
show BST t
EmptyBST = String
"E"
  show (ForkBST BST l
l Node n a
n BST r
r) = String
"F " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BST l -> String
forall (t :: Tree). BST t -> String
go BST 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]
++ BST r -> String
forall (t :: Tree). BST t -> String
go BST r
r
    where
      go :: BST t' -> String
      go :: forall (t :: Tree). BST t -> String
go BST t'
EmptyBST = String
"E"
      go (ForkBST BST l
l' Node n a
n' BST r
r') = String
"(F " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BST l -> String
forall (t :: Tree). BST t -> String
go BST 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]
++ BST r -> String
forall (t :: Tree). BST t -> String
go BST r
r' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"