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

-- |
-- Module      : Data.Tree.AVL.Intern.Constructor
-- Description : Constructor of type safe internalist AVL 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 AVL
-- trees and instance definition for the `Show` type class.
module Data.Tree.AVL.Intern.Constructors
  ( AVL (EmptyAVL, ForkAVL),
    AlmostAVL (AlmostAVL),
  )
where

import Data.Kind (Type)
import Data.Tree.AVL.Invariants (BalancedHeights, Height)
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 `AVL` trees. Given two `AVL` 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 and if the heights are balanced.
-- Notice that, by inductive reasoning, this is all that's needed to assert that the new tree is a `AVL`.
data AVL :: Tree -> Type where
  EmptyAVL :: AVL 'EmptyTree
  ForkAVL ::
    (Show a, LtN l n ~ 'True, GtN r n ~ 'True, BalancedHeights (Height l) (Height r) n ~ 'True) =>
    AVL l ->
    Node n a ->
    AVL r ->
    AVL ('ForkTree l (Node n a) r)

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

-- | Constructor of `AlmostAVL` tress. This kind of trees arises after
-- an insertion or deletion over an `AVL` that may leave
-- the tree unbalanced.
data AlmostAVL :: Tree -> Type where
  AlmostAVL ::
    (Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
    AVL l ->
    Node n a ->
    AVL r ->
    AlmostAVL ('ForkTree l (Node n a) r)