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

-- |
-- Module      : Data.Tree.BST.Extern
-- Description : Interface for externalist 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 externalist approach.
module Data.Tree.BST.Extern
  ( emptyBST,
    insertBST,
    lookupBST,
    deleteBST,
  )
where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.BST.Extern.Constructors (BST (BST), IsBSTT (EmptyIsBSTT))
import Data.Tree.BST.Extern.Delete (Deletable (Delete, delete))
import Data.Tree.BST.Extern.DeleteProofs (ProofIsBSTDelete (proofIsBSTDelete))
import Data.Tree.BST.Extern.Insert (Insertable (Insert, insert))
import Data.Tree.BST.Extern.InsertProofs (ProofIsBSTInsert (proofIsBSTInsert))
import Data.Tree.BST.Extern.Lookup (Lookupable (lookup))
import Data.Tree.BST.Utils (Member)
import Data.Tree.ITree
  ( ITree (EmptyITree),
    Tree (EmptyTree, ForkTree),
  )
import Data.Tree.Node (Node, mkNode)
import Prelude (Bool (True))

-- | Empty `BST` tree with the externalist implementation.
emptyBST :: BST 'EmptyTree
emptyBST :: BST 'EmptyTree
emptyBST = ITree 'EmptyTree -> IsBSTT 'EmptyTree -> BST 'EmptyTree
forall (t :: Tree). ITree t -> IsBSTT t -> BST t
BST ITree 'EmptyTree
EmptyITree IsBSTT 'EmptyTree
EmptyIsBSTT

-- | Interface for the insertion algorithm in the externalist implementation.
-- It calls `insert` over `ITree` and `proofIsBSTInsert` for constructing the evidence
-- that the new tree remains `BST`.
insertBST ::
  (Insertable x a t, ProofIsBSTInsert x a t) =>
  Proxy x ->
  a ->
  BST t ->
  BST (Insert x a t)
insertBST :: forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST (Proxy x
px :: Proxy x) (a
a :: a) (BST ITree t
t IsBSTT t
tIsBST) = ITree (Insert x a t) -> IsBSTT (Insert x a t) -> BST (Insert x a t)
forall (t :: Tree). ITree t -> IsBSTT t -> BST t
BST (Node x a -> ITree t -> ITree (Insert x a t)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> ITree t -> ITree (Insert x a t)
insert Node x a
node ITree t
t) (Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
forall (x :: Nat) a (t :: Tree).
ProofIsBSTInsert x a t =>
Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT t
tIsBST)
  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
px a
a
    pNode :: Proxy (Node x a)
pNode = Proxy (Node x a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node x a)

-- | Interface for the lookup algorithm in the externalist implementation of `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
p (BST ITree t
t IsBSTT t
_) = Proxy x -> ITree 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 -> ITree t -> a
lookup Proxy x
p ITree t
t

-- | Interface for the deletion algorithm in the externalist implementation.
-- It calls `delete` over `ITree` and `proofIsBSTDelete` for constructing the evidence
-- that the new tree remains `BST`.
deleteBST ::
  (Deletable x t, ProofIsBSTDelete x t) =>
  Proxy x ->
  BST t ->
  BST (Delete x t)
deleteBST :: forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy x
px (BST ITree t
t IsBSTT t
tIsBST) = ITree (Delete x t) -> IsBSTT (Delete x t) -> BST (Delete x t)
forall (t :: Tree). ITree t -> IsBSTT t -> BST t
BST (Proxy x -> ITree t -> ITree (Delete x t)
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> ITree t -> ITree (Delete x t)
delete Proxy x
px ITree t
t) (Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
forall (x :: Nat) (t :: Tree).
ProofIsBSTDelete x t =>
Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
proofIsBSTDelete Proxy x
px IsBSTT t
tIsBST)