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

-- |
-- Module      : Data.Tree.BST.Extern.Lookup
-- Description : Lookup 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 lookup algorithm over ITree trees for
-- externalist BST trees.
module Data.Tree.BST.Extern.Lookup
  ( Lookupable (lookup),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.BST.Utils (LookupValueType, Member)
import Data.Tree.ITree (ITree (ForkITree), Tree (ForkTree))
import Data.Tree.Node (Node, getValue)
import GHC.TypeNats (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 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`.
-- 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 the given key in the tree.
  lookup ::
    (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True) =>
    Proxy x ->
    ITree t ->
    a

instance
  ( t ~ 'ForkTree l (Node n a1) r,
    a ~ LookupValueType x t t,
    o ~ CmpNat x n,
    Lookupable' x a ('ForkTree l (Node n a1) r) o
  ) =>
  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 -> ITree ('ForkTree l (Node n a1) r) -> a
lookup Proxy x
x ITree ('ForkTree l (Node n a1) r)
t = Proxy x -> ITree ('ForkTree l (Node n a1) r) -> Proxy o -> a
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Lookupable' x a t o =>
Proxy x -> ITree t -> Proxy o -> a
lookup' Proxy x
x 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 lookup a node with key @x@
-- in a non empty tree @t@ without checking any structural invariant (key ordering).
-- 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 -> ITree t -> Proxy o -> a

instance Lookupable' x a ('ForkTree l (Node n a) r) 'EQ where
  lookup' :: Proxy x -> ITree ('ForkTree l (Node n a) r) -> Proxy 'EQ -> a
lookup' Proxy x
_ (ForkITree ITree l
_ Node n a
node ITree 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
-> ITree ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> a
lookup' Proxy x
p (ForkITree ITree l
l Node n a
_ ITree r
_) Proxy 'LT
_ = Proxy x -> ITree l -> Proxy o -> a
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Lookupable' x a t o =>
Proxy x -> ITree t -> Proxy o -> a
lookup' Proxy x
p ITree 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 ('ForkTree rl (Node rn rna) rr) o
  ) =>
  Lookupable' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  lookup' :: Proxy x
-> ITree ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> a
lookup' Proxy x
p (ForkITree ITree l
_ Node n a
_ ITree r
r) Proxy 'GT
_ = Proxy x -> ITree r -> Proxy o -> a
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Lookupable' x a t o =>
Proxy x -> ITree t -> Proxy o -> a
lookup' Proxy x
p ITree r
r (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)