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

-- |
-- Module      : Data.Tree.AVL.Intern.Lookup
-- Description : Lookup algorithm over internalist AVL trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the lookup algorithm over internalist AVL trees.
-- Since the lookup does not modify the tree, there is no need for proofs.
module Data.Tree.AVL.Intern.Lookup
  ( Lookupable (lookup),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Intern.Constructors (AVL (ForkAVL))
import Data.Tree.BST.Utils (LookupValueType, Member)
import Data.Tree.ITree (Tree (ForkTree))
import Data.Tree.Node (Node, getValue)
import GHC.TypeLits (CmpNat, Nat)
import Prelude
  ( Bool (True),
    Ordering (EQ, GT, LT),
  )

-- | This type class provides the functionality to lookup a node with key @x@
-- in a non empty `AVL` @t@.
-- The lookup is defined at the value level and the type level.
-- It's necessary to know the type @a@ of the value stored in node with key @x@
-- so that the type of the value returned by 'lookup' may be specified.
class Lookupable (x :: Nat) (a :: Type) (t :: Tree) where
  lookup ::
    (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True) =>
    Proxy x ->
    AVL t ->
    a

instance
  (t ~ 'ForkTree l (Node n a1) r, a ~ LookupValueType x t t, Lookupable' x a t (CmpNat x n)) =>
  Lookupable x a ('ForkTree l (Node n a1) r)
  where
  lookup :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) r ~ 'ForkTree l (Node n a1) r,
 Member x ('ForkTree l (Node n a1) r) ('ForkTree l (Node n a1) r)
 ~ 'True) =>
Proxy x -> AVL ('ForkTree l (Node n a1) r) -> a
lookup Proxy x
x AVL ('ForkTree l (Node n a1) r)
t = Proxy x
-> AVL ('ForkTree l (Node n a1) r) -> Proxy (CmpNat x n) -> a
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Lookupable' x a t o =>
Proxy x -> AVL t -> Proxy o -> a
lookup' Proxy x
x AVL ('ForkTree l (Node n a1) r)
t (Proxy (CmpNat x n)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (CmpNat x n))

-- | This type class provides the functionality to lookup a node with key @x@
-- in a non empty `AVL` @t@.
-- It's only used by the 'Lookupable' 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 lookup.
class Lookupable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
  lookup' :: Proxy x -> AVL t -> Proxy o -> a

instance Lookupable' x a ('ForkTree l (Node n a) r) 'EQ where
  lookup' :: Proxy x -> AVL ('ForkTree l (Node n a) r) -> Proxy 'EQ -> a
lookup' Proxy x
_ (ForkAVL AVL l
_ Node n a
node AVL r
_) Proxy 'EQ
_ = Node n a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node n a
node

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    Lookupable' x a l o
  ) =>
  Lookupable' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT
  where
  lookup' :: Proxy x
-> AVL ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> a
lookup' Proxy x
p (ForkAVL AVL l
l Node n a
_ AVL r
_) Proxy 'LT
_ = Proxy x -> AVL l -> Proxy o -> a
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Lookupable' x a t o =>
Proxy x -> AVL t -> Proxy o -> a
lookup' Proxy x
p AVL l
l (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    Lookupable' x a r o
  ) =>
  Lookupable' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  lookup' :: Proxy x
-> AVL ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> a
lookup' Proxy x
p (ForkAVL AVL l
_ Node n a
_ AVL r
r) Proxy 'GT
_ = Proxy x -> AVL r -> Proxy o -> a
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Lookupable' x a t o =>
Proxy x -> AVL t -> Proxy o -> a
lookup' Proxy x
p AVL r
r (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)