{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      : Data.Tree.BST.Extern.Delete
-- Description : Deletion algorithm over ITree trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the deletion algorithm over ITree trees for
-- externalist BST trees.
module Data.Tree.BST.Extern.Delete
  ( Maxable (MaxKey, MaxValue, maxValue),
    MaxKeyDeletable (MaxKeyDelete, maxKeyDelete),
    Deletable (Delete, delete),
    Deletable' (Delete', delete'),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.ITree
  ( ITree (EmptyITree, ForkITree),
    Tree (EmptyTree, ForkTree),
  )
import Data.Tree.Node (Node, getValue, mkNode)
import GHC.TypeNats (CmpNat, Nat)
import Prelude (Ordering (EQ, GT, LT), Show)

-- | This type class provides the functionality to delete the node with maximum key value
-- in a tree @t@ without checking any structural invariant (key ordering).
-- The deletion is defined at the value level and the type level, and is performed
-- as if the tree is a `Data.Tree.BST.Extern.Constructors.BST`; the verification of the @BST@ restrictions is performed after the deletion.
class MaxKeyDeletable (t :: Tree) where
  type MaxKeyDelete (t :: Tree) :: Tree
  maxKeyDelete ::
    (t ~ 'ForkTree l (Node n a1) r) =>
    ITree t ->
    ITree (MaxKeyDelete t)

instance MaxKeyDeletable 'EmptyTree where
  type MaxKeyDelete 'EmptyTree = 'EmptyTree
  maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('EmptyTree ~ 'ForkTree l (Node n a1) r) =>
ITree 'EmptyTree -> ITree (MaxKeyDelete 'EmptyTree)
maxKeyDelete ITree 'EmptyTree
_ = ITree 'EmptyTree
ITree (MaxKeyDelete 'EmptyTree)
EmptyITree

instance MaxKeyDeletable ('ForkTree l (Node n a1) 'EmptyTree) where
  type MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree) = l
  maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) 'EmptyTree ~ 'ForkTree l (Node n a1) r) =>
ITree ('ForkTree l (Node n a1) 'EmptyTree)
-> ITree (MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree))
maxKeyDelete (ForkITree ITree l
l Node n a
_ ITree r
_) = ITree l
ITree (MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree))
l

instance
  (MaxKeyDeletable ('ForkTree rl (Node rn ra) rr)) =>
  MaxKeyDeletable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
  where
  type
    MaxKeyDelete ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) =
      'ForkTree l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
  maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a1) r) =>
ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> ITree
     (MaxKeyDelete
        ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)))
maxKeyDelete (ForkITree ITree l
l Node n a
node ITree r
r) =
    ITree l
-> Node n a
-> ITree (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
-> ITree
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
Show a =>
ITree l -> Node n a -> ITree r -> ITree ('ForkTree l (Node n a) r)
ForkITree ITree l
l Node n a
node (ITree r -> ITree (MaxKeyDelete r)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
ITree t -> ITree (MaxKeyDelete t)
maxKeyDelete ITree r
r)

-- | This type class provides the functionality to get the key, type and value of the node with maximum key value
-- in a tree @t@ without checking any structural invariant (key ordering).
-- The lookup is defined at the value level and the type level, and is performed
-- as if the tree is a `Data.Tree.BST.Extern.Constructors.BST`.
-- Since the keys are only kept at the type level, there's no value level getter of the maximum key.
class Maxable (t :: Tree) where
  type MaxKey (t :: Tree) :: Nat
  type MaxValue (t :: Tree) :: Type
  maxValue ::
    (t ~ 'ForkTree l (Node n a1) r) =>
    ITree t ->
    MaxValue t

instance Maxable ('ForkTree l (Node n a1) 'EmptyTree) where
  type MaxKey ('ForkTree l (Node n a1) 'EmptyTree) = n
  type MaxValue ('ForkTree l (Node n a1) 'EmptyTree) = a1
  maxValue :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) 'EmptyTree ~ 'ForkTree l (Node n a1) r) =>
ITree ('ForkTree l (Node n a1) 'EmptyTree)
-> MaxValue ('ForkTree l (Node n a1) 'EmptyTree)
maxValue (ForkITree ITree l
_ Node n a
node ITree r
EmptyITree) = Node n a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node n a
node

instance
  (Maxable ('ForkTree rl (Node rn ra) rr)) =>
  Maxable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
  where
  type MaxKey ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) = MaxKey ('ForkTree rl (Node rn ra) rr)
  type MaxValue ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) = MaxValue ('ForkTree rl (Node rn ra) rr)
  maxValue :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a1) r) =>
ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> MaxValue
     ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
maxValue (ForkITree ITree l
_ Node n a
_ ITree r
r) = ITree r -> MaxValue r
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
ITree t -> MaxValue t
maxValue ITree r
r

-- | This type class provides the functionality to delete the node with key @x@
-- in a tree @t@ without checking any structural invariant (key ordering).
-- The deletion is defined at the value level and the type level, and is performed
-- as if the tree is a `Data.Tree.BST.Extern.Constructors.BST`; the key ordering is verified after the deletion.
class Deletable (x :: Nat) (t :: Tree) where
  type Delete (x :: Nat) (t :: Tree) :: Tree

  -- | Delete the node with the given key.
  -- If the key is not in the tree, return the same tree.
  delete :: Proxy x -> ITree t -> ITree (Delete x t)

instance Deletable x 'EmptyTree where
  type Delete x 'EmptyTree = 'EmptyTree
  delete :: Proxy x -> ITree 'EmptyTree -> ITree (Delete x 'EmptyTree)
delete Proxy x
_ ITree 'EmptyTree
_ = ITree 'EmptyTree
ITree (Delete x 'EmptyTree)
EmptyITree

instance
  ( o ~ CmpNat x n,
    Deletable' x ('ForkTree l (Node n a1) r) o
  ) =>
  Deletable x ('ForkTree l (Node n a1) r)
  where
  type Delete x ('ForkTree l (Node n a1) r) = Delete' x ('ForkTree l (Node n a1) r) (CmpNat x n)
  delete :: Proxy x
-> ITree ('ForkTree l (Node n a1) r)
-> ITree (Delete x ('ForkTree l (Node n a1) r))
delete Proxy x
px ITree ('ForkTree l (Node n a1) r)
t = Proxy x
-> ITree ('ForkTree l (Node n a1) r)
-> Proxy o
-> ITree (Delete' x ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> ITree t -> Proxy o -> ITree (Delete' x t o)
delete' Proxy x
px ITree ('ForkTree l (Node n a1) r)
t (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)

-- | This type class provides the functionality to delete a node with key @x@
-- in a non empty tree @t@ without checking any structural invariant (key ordering).
-- It's only used by the 'Deletable' type class and it has one extra parameter @o@,
-- which is the type level comparison of @x@ with the key value of the root node.
-- The @o@ parameter guides the deletion.
class Deletable' (x :: Nat) (t :: Tree) (o :: Ordering) where
  type Delete' (x :: Nat) (t :: Tree) (o :: Ordering) :: Tree
  delete' :: Proxy x -> ITree t -> Proxy o -> ITree (Delete' x t o)

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ where
  type Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ = 'EmptyTree
  delete' :: Proxy x
-> ITree ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> ITree
     (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
delete' Proxy x
_ ITree ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
_ Proxy 'EQ
_ = ITree 'EmptyTree
ITree (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
EmptyITree

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ where
  type Delete' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ = 'ForkTree rl (Node rn ra) rr
  delete' :: Proxy x
-> ITree
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> ITree
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
delete' Proxy x
_ (ForkITree ITree l
_ Node n a
_ ITree r
r) Proxy 'EQ
_ = ITree r
ITree
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
r

instance Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ where
  type Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ = 'ForkTree ll (Node ln la) lr
  delete' :: Proxy x
-> ITree
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> ITree
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
        'EQ)
delete' Proxy x
_ (ForkITree ITree l
l Node n a
_ ITree r
_) Proxy 'EQ
_ = ITree l
ITree
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
     'EQ)
l

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    Show (MaxValue l),
    MaxKeyDeletable l,
    Maxable l
  ) =>
  Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ
  where
  type
    Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ =
      'ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node (MaxKey ('ForkTree ll (Node ln la) lr)) (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr)
  delete' :: Proxy x
-> ITree
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n a1)
        ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> ITree
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
delete' Proxy x
_ (ForkITree ITree l
l Node n a
_ ITree r
r) Proxy 'EQ
_ =
    ITree (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
-> ITree r
-> ITree
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
Show a =>
ITree l -> Node n a -> ITree r -> ITree ('ForkTree l (Node n a) r)
ForkITree ITree (MaxKeyDelete l)
ITree (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
l' Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' ITree r
r
    where
      l' :: ITree (MaxKeyDelete l)
l' = ITree l -> ITree (MaxKeyDelete l)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
ITree t -> ITree (MaxKeyDelete t)
maxKeyDelete ITree l
l
      node' :: Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' = Proxy (MaxKey ('ForkTree ll (Node ln la) lr))
-> MaxValue ('ForkTree ll (Node ln la) lr)
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy (MaxKey l)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (MaxKey l)) (ITree l -> MaxValue l
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
ITree t -> MaxValue t
maxValue ITree l
l)

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT where
  type Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT = ('ForkTree 'EmptyTree (Node n a1) r)
  delete' :: Proxy x
-> ITree ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> ITree (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
delete' Proxy x
_ ITree ('ForkTree 'EmptyTree (Node n a1) r)
t Proxy 'LT
_ = ITree ('ForkTree 'EmptyTree (Node n a1) r)
ITree (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
t

instance
  ( o ~ CmpNat x ln,
    Deletable' x ('ForkTree ll (Node ln la) lr) o
  ) =>
  Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT
  where
  type
    Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT =
      'ForkTree (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln)) (Node n a1) r
  delete' :: Proxy x
-> ITree ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r)
-> Proxy 'LT
-> ITree
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT)
delete' Proxy x
px (ForkITree ITree l
l Node n a
node ITree r
r) Proxy 'LT
_ = ITree (Delete' x ('ForkTree ll (Node ln la) lr) o)
-> Node n a
-> ITree r
-> ITree
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
Show a =>
ITree l -> Node n a -> ITree r -> ITree ('ForkTree l (Node n a) r)
ForkITree (Proxy x -> ITree l -> Proxy o -> ITree (Delete' x l o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> ITree t -> Proxy o -> ITree (Delete' x t o)
delete' Proxy x
px ITree l
l (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) Node n a
node ITree r
r

instance Deletable' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT where
  type Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT = ('ForkTree l (Node n a1) 'EmptyTree)
  delete' :: Proxy x
-> ITree ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> ITree (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
delete' Proxy x
_ ITree ('ForkTree l (Node n a1) 'EmptyTree)
t Proxy 'GT
_ = ITree ('ForkTree l (Node n a1) 'EmptyTree)
ITree (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
t

instance
  ( o ~ CmpNat x rn,
    Deletable' x ('ForkTree rl (Node rn ra) rr) o
  ) =>
  Deletable' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT
  where
  type
    Delete' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT =
      'ForkTree l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn))
  delete' :: Proxy x
-> ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'GT
-> ITree
     (Delete'
        x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT)
delete' Proxy x
px (ForkITree ITree l
l Node n a
node ITree r
r) Proxy 'GT
_ = ITree l
-> Node n a
-> ITree (Delete' x ('ForkTree rl (Node rn ra) rr) o)
-> ITree
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
Show a =>
ITree l -> Node n a -> ITree r -> ITree ('ForkTree l (Node n a) r)
ForkITree ITree l
l Node n a
node (Proxy x -> ITree r -> Proxy o -> ITree (Delete' x r o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> ITree t -> Proxy o -> ITree (Delete' x t o)
delete' Proxy x
px ITree r
r (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o))