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

-- |
-- Module      : Data.Tree.AVL.Extern.Insert
-- Description : Insertion 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 insertion algorithm over ITree trees for
-- externalist AVL trees.
module Data.Tree.AVL.Extern.Insert
  ( Insertable (Insert, insert),
    Insertable' (Insert'),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Extern.Balance (Balanceable (Balance, balance))
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 insert a node with key @x@ and value type @a@
-- in a tree @t@ without checking any structural invariant (key ordering or height balance).
-- The insertion is defined at the value level and the type level, and is performed
-- as if the tree is an `Data.Tree.AVL.Extern.AVL`; the verification of the @AVL@ restrictions is performed after the insertion.
class Insertable (x :: Nat) (a :: Type) (t :: Tree) where
  type Insert (x :: Nat) (a :: Type) (t :: Tree) :: Tree

  -- | Insert a new node.
  -- If the key is already present in the tree, update the value.
  insert :: Node x a -> ITree t -> ITree (Insert x a t)

instance
  (Show a) =>
  Insertable x a 'EmptyTree
  where
  type Insert x a 'EmptyTree = 'ForkTree 'EmptyTree (Node x a) 'EmptyTree
  insert :: Node x a -> ITree 'EmptyTree -> ITree (Insert x a 'EmptyTree)
insert Node x a
node ITree 'EmptyTree
_ = ITree 'EmptyTree
-> Node x a
-> ITree 'EmptyTree
-> ITree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
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 'EmptyTree
EmptyITree Node x a
node ITree 'EmptyTree
EmptyITree

instance
  ( o ~ CmpNat x n,
    Insertable' x a ('ForkTree l (Node n a1) r) o
  ) =>
  Insertable x a ('ForkTree l (Node n a1) r)
  where
  type Insert x a ('ForkTree l (Node n a1) r) = Insert' x a ('ForkTree l (Node n a1) r) (CmpNat x n)
  insert :: Node x a
-> ITree ('ForkTree l (Node n a1) r)
-> ITree (Insert x a ('ForkTree l (Node n a1) r))
insert Node x a
node ITree ('ForkTree l (Node n a1) r)
t = Node x a
-> ITree ('ForkTree l (Node n a1) r)
-> Proxy o
-> ITree (Insert' x a ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> ITree t -> Proxy o -> ITree (Insert' x a t o)
insert' Node x a
node 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 insert a node with key @x@ and value type @a@
-- in a non empty tree @t@ without checking any structural invariant (key ordering or height balance).
-- It's only used by the 'Insertable' 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 insertion.
class Insertable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
  type Insert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) :: Tree
  insert' :: Node x a -> ITree t -> Proxy o -> ITree (Insert' x a t o)

instance
  (Show a) =>
  Insertable' x a ('ForkTree l (Node n a1) r) 'EQ
  where
  type Insert' x a ('ForkTree l (Node n a1) r) 'EQ = 'ForkTree l (Node n a) r
  insert' :: Node x a
-> ITree ('ForkTree l (Node n a1) r)
-> Proxy 'EQ
-> ITree (Insert' x a ('ForkTree l (Node n a1) r) 'EQ)
insert' Node x a
node (ForkITree ITree l
l Node n a
_ ITree r
r) Proxy 'EQ
_ = ITree l -> Node n a -> ITree r -> ITree ('ForkTree l (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 ITree l
l Node n a
node' ITree r
r
    where
      node' :: Node n a
node' = Proxy n -> a -> Node n a
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Node x a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node x a
node)

instance
  (Show a, Balanceable ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r)) =>
  Insertable' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT
  where
  type Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT = Balance ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r)
  insert' :: Node x a
-> ITree ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> ITree (Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
insert' Node x a
node (ForkITree ITree l
_ Node n a
node' ITree r
r) Proxy 'LT
_ = ITree
  ('ForkTree
     ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
-> ITree
     (Balance
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r))
forall (t :: Tree). Balanceable t => ITree t -> ITree (Balance t)
balance (ITree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Node n a
-> ITree r
-> ITree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (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 (ITree 'EmptyTree
-> Node x a
-> ITree 'EmptyTree
-> ITree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
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 'EmptyTree
EmptyITree Node x a
node ITree 'EmptyTree
EmptyITree) Node n a
node' ITree r
r)

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    Insertable' x a l o,
    Balanceable ('ForkTree (Insert' x a l o) (Node n a1) r)
  ) =>
  Insertable' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT
  where
  type
    Insert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT =
      Balance ('ForkTree (Insert' x a ('ForkTree ll (Node ln lna) lr) (CmpNat x ln)) (Node n a1) r)
  insert' :: Node x a
-> ITree ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> ITree
     (Insert'
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT)
insert' Node x a
node (ForkITree ITree l
l Node n a
node' ITree r
r) Proxy 'LT
_ =
    ITree
  ('ForkTree
     (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> ITree
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r))
forall (t :: Tree). Balanceable t => ITree t -> ITree (Balance t)
balance (ITree (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Node n a
-> ITree r
-> ITree
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) 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 (Node x a -> ITree l -> Proxy o -> ITree (Insert' x a l o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> ITree t -> Proxy o -> ITree (Insert' x a t o)
insert' Node x a
node ITree l
l (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) Node n a
node' ITree r
r)

instance
  (Show a, Balanceable ('ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))) =>
  Insertable' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT
  where
  type Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT = Balance ('ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
  insert' :: Node x a
-> ITree ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> ITree (Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
insert' Node x a
node (ForkITree ITree l
l Node n a
node' ITree r
_) Proxy 'GT
_ = ITree
  ('ForkTree
     l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
-> ITree
     (Balance
        ('ForkTree
           l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)))
forall (t :: Tree). Balanceable t => ITree t -> ITree (Balance t)
balance (ITree l
-> Node n a
-> ITree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> ITree
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
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 'EmptyTree
-> Node x a
-> ITree 'EmptyTree
-> ITree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
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 'EmptyTree
EmptyITree Node x a
node ITree 'EmptyTree
EmptyITree))

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    Insertable' x a r o,
    Balanceable ('ForkTree l (Node n a1) (Insert' x a r o))
  ) =>
  Insertable' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  type
    Insert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT =
      Balance ('ForkTree l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) (CmpNat x rn)))
  insert' :: Node x a
-> ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> ITree
     (Insert'
        x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT)
insert' Node x a
node (ForkITree ITree l
l Node n a
node' ITree r
r) Proxy 'GT
_ =
    ITree
  ('ForkTree
     l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> ITree
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
forall (t :: Tree). Balanceable t => ITree t -> ITree (Balance t)
balance (ITree l
-> Node n a
-> ITree (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> ITree
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) 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' (Node x a -> ITree r -> Proxy o -> ITree (Insert' x a r o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> ITree t -> Proxy o -> ITree (Insert' x a t o)
insert' Node x a
node ITree r
r (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)))