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

-- |
-- Module      : Data.Tree.AVL.Extern
-- Description : Interface for externalist type safe AVL 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 AVL trees
-- implemented with the externalist approach.
module Data.Tree.AVL.Extern
  ( emptyAVL,
    insertAVL,
    lookupAVL,
    deleteAVL,
  )
where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Extern.Constructors (AVL (AVL), IsBalancedT (EmptyIsBalancedT))
import Data.Tree.AVL.Extern.Delete (Deletable (Delete, delete))
import Data.Tree.AVL.Extern.DeleteProofs
  ( ProofIsBSTDelete (proofIsBSTDelete),
    ProofIsBalancedDelete (proofIsBalancedDelete),
  )
import Data.Tree.AVL.Extern.Insert (Insertable (Insert, insert))
import Data.Tree.AVL.Extern.InsertProofs
  ( ProofIsBSTInsert (proofIsBSTInsert),
    ProofIsBalancedInsert (proofIsBalancedInsert),
  )
import Data.Tree.BST.Extern.Constructors (IsBSTT (EmptyIsBSTT))
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 `AVL` tree with the externalist implementation.
emptyAVL :: AVL 'EmptyTree
emptyAVL :: AVL 'EmptyTree
emptyAVL = ITree 'EmptyTree
-> IsBSTT 'EmptyTree -> IsBalancedT 'EmptyTree -> AVL 'EmptyTree
forall (t :: Tree). ITree t -> IsBSTT t -> IsBalancedT t -> AVL t
AVL ITree 'EmptyTree
EmptyITree IsBSTT 'EmptyTree
EmptyIsBSTT IsBalancedT 'EmptyTree
EmptyIsBalancedT

-- | Interface for the insertion algorithm in the externalist implementation.
-- It calls `insert` over `ITree`, and `proofIsBSTInsert` and `proofIsBalancedInsert` for constructing the evidence
-- that the new tree remains `AVL`.
insertAVL ::
  (Insertable x a t, ProofIsBSTInsert x a t, ProofIsBalancedInsert x a t) =>
  Proxy x ->
  a ->
  AVL t ->
  AVL (Insert x a t)
insertAVL :: forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t,
 ProofIsBalancedInsert x a t) =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy x
px :: Proxy x) (a
a :: a) (AVL ITree t
t IsBSTT t
tIsBST IsBalancedT t
tIsBalanced) = ITree (Insert x a t)
-> IsBSTT (Insert x a t)
-> IsBalancedT (Insert x a t)
-> AVL (Insert x a t)
forall (t :: Tree). ITree t -> IsBSTT t -> IsBalancedT t -> AVL t
AVL (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) (Proxy (Node x a) -> IsBalancedT t -> IsBalancedT (Insert x a t)
forall (x :: Nat) a (t :: Tree).
ProofIsBalancedInsert x a t =>
Proxy (Node x a) -> IsBalancedT t -> IsBalancedT (Insert x a t)
proofIsBalancedInsert Proxy (Node x a)
pNode IsBalancedT t
tIsBalanced)
  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 `AVL`.
lookupAVL ::
  (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True, Lookupable x a t) =>
  Proxy x ->
  AVL t ->
  a
lookupAVL :: 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 -> AVL t -> a
lookupAVL Proxy x
p (AVL ITree t
t IsBSTT t
_ IsBalancedT 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` and `proofIsBalancedDelete`  for constructing the evidence
-- that the new tree remains `AVL`.
deleteAVL ::
  (Deletable x t, ProofIsBSTDelete x t, ProofIsBalancedDelete x t) =>
  Proxy x ->
  AVL t ->
  AVL (Delete x t)
deleteAVL :: forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t, ProofIsBalancedDelete x t) =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL Proxy x
px (AVL ITree t
t IsBSTT t
tIsBST IsBalancedT t
tIsBalanced) = ITree (Delete x t)
-> IsBSTT (Delete x t)
-> IsBalancedT (Delete x t)
-> AVL (Delete x t)
forall (t :: Tree). ITree t -> IsBSTT t -> IsBalancedT t -> AVL t
AVL (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) (Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t)
forall (x :: Nat) (t :: Tree).
ProofIsBalancedDelete x t =>
Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t)
proofIsBalancedDelete Proxy x
px IsBalancedT t
tIsBalanced)