Data.Tree.BST.Extern.Constructors

Implementation of the constructor of type safe externalist BST trees and instance definition for the Show type class.

Documentation

data BST :: Tree -> Type where

Constructor of BST trees. Given an arbitrary ITree, it constructs a new BST together with the proof term IsBSTT which shows that the keys are ordered.

Constructors

BST :: ITree t -> IsBSTT t -> BST t

Instances

Show (BST t)

Instance definition for the Show type class. It relies on the instance for ITree.

Defined in Data.Tree.BST.Extern.Constructors

Methods

showsPrec :: Int -> BST t -> ShowS

show :: BST t -> String

showList :: [BST t] -> ShowS

mkBST :: IsBSTC t => ITree t -> BST t

Given an ITree, compute the proof term IsBSTT, through the type class IsBSTC, in order to check if it is a BST tree. This is the fully externalist constructor for BST trees.

data IsBSTT :: Tree -> Type where

Proof term which shows that t is a BST. The restrictions on the constructor ForkIsBSTT are verified at compile time. Given two proofs of BST and an arbitrary node, it tests wether the key of the node verifies the LtN and GtN invariants. Notice that this is all that's needed to assert that the new tree is a BST, since, both left and right proofs are evidence of the key ordering in both left and right sub trees.

Constructors

EmptyIsBSTT :: IsBSTT 'EmptyTree

ForkIsBSTT :: (LtN l n ~ 'True, GtN r n ~ 'True) => IsBSTT l -> Proxy (Node n a) -> IsBSTT r -> IsBSTT ('ForkTree l (Node n a) r)

class IsBSTC (t :: Tree) where

Type class for automatically constructing the proof term IsBSTT.

Methods

isBSTT :: IsBSTT t

Instances

IsBSTC 'EmptyTree

Instances for the type class IsBSTC.

Defined in Data.Tree.BST.Extern.Constructors

Methods

isBSTT :: IsBSTT 'EmptyTree

(IsBSTC l, IsBSTC r, LtN l n ~ 'True, GtN r n ~ 'True) => IsBSTC ('ForkTree l (Node n a) r)

Defined in Data.Tree.BST.Extern.Constructors

Methods

isBSTT :: IsBSTT ('ForkTree l (Node n a) r)