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

-- |
-- Module      : Data.Tree.BST.Intern
-- Description : Interface for internalist type safe BST trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Interface for the main functions over type safe BST trees
-- implemented with the internalist approach.
module Data.Tree.BST.Intern
  ( emptyBST,
    insertBST,
    lookupBST,
    deleteBST,
  )
where

import Data.Proxy (Proxy)
import Data.Tree.BST.Intern.Constructors (BST (EmptyBST))
import Data.Tree.BST.Intern.Delete (Deletable (Delete, delete))
import Data.Tree.BST.Intern.Insert (Insertable (Insert, insert))
import Data.Tree.BST.Intern.Lookup (Lookupable (lookup))
import Data.Tree.BST.Utils (Member)
import Data.Tree.ITree (Tree (EmptyTree, ForkTree))
import Data.Tree.Node (Node, mkNode)
import Prelude (Bool (True))

-- | Empty `BST` tree with the internalist implementation.
emptyBST :: BST 'EmptyTree
emptyBST :: BST 'EmptyTree
emptyBST = BST 'EmptyTree
EmptyBST

-- | Interface for the insertion algorithm in the internalist implementation.
-- It calls `insert` over an internalist `BST` tree.
insertBST ::
  (Insertable x a t) =>
  Proxy x ->
  a ->
  BST t ->
  BST (Insert x a t)
insertBST :: forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy x
x a
a = Node x a -> BST t -> BST (Insert x a t)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> BST t -> BST (Insert x a t)
insert Node x a
node
  where
    node :: Node x a
node = Proxy x -> a -> Node x a
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode Proxy x
x a
a

-- | Interface for the lookup algorithm in the internalist implementation for `BST`.
lookupBST ::
  (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True, Lookupable x a t) =>
  Proxy x ->
  BST t ->
  a
lookupBST :: forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree) (x :: Nat)
       a.
(t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True,
 Lookupable x a t) =>
Proxy x -> BST t -> a
lookupBST = Proxy x -> BST t -> a
forall (x :: Nat) a (t :: Tree) (l :: Tree) (n :: Nat) a1
       (r :: Tree).
(Lookupable x a t, t ~ 'ForkTree l (Node n a1) r,
 Member x t t ~ 'True) =>
Proxy x -> BST t -> a
lookup

-- | Interface for the deletion algorithm in the internalist implementation.
-- It calls `delete` over an internalist `BST` tree.
deleteBST ::
  (Deletable x t) =>
  Proxy x ->
  BST t ->
  BST (Delete x t)
deleteBST :: forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST = Proxy x -> BST t -> BST (Delete x t)
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> BST t -> BST (Delete x t)
delete