Data.Tree.AVL.Intern.Lookup

Implementation of the lookup algorithm over internalist AVL trees. Since the lookup does not modify the tree, there is no need for proofs.

Documentation

class Lookupable (x :: Nat) (a :: Type) (t :: Tree) where

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.

Methods

lookup :: (t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True) => Proxy x -> AVL t -> a

Instances

(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)

Defined in Data.Tree.AVL.Intern.Lookup

Methods

lookup :: forall (l0 :: Tree) (n0 :: Nat) a10 (r0 :: Tree). ('ForkTree l (Node n a1) r ~ 'ForkTree l0 (Node n0 a10) r0, 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

class Lookupable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where

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.

Methods

lookup' :: Proxy x -> AVL t -> Proxy o -> a