Copyright | (c) Nicolás Rodríguez 2021 |
---|---|
License | GPL-3 |
Maintainer | Nicolás Rodríguez |
Stability | experimental |
Portability | POSIX |
Safe Haskell | Safe |
Language | Haskell2010 |
Implementation of the insertion algorithm over internalist BST trees, along with the necessary proofs to ensure (at compile time) that the key ordering still holds.
Synopsis
- class Insertable (x :: Nat) (a :: Type) (t :: Tree) where
- class Insertable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
- class ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
- class ProofGtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
Documentation
class Insertable (x :: Nat) (a :: Type) (t :: Tree) where Source #
This type class provides the functionality to insert a node with key x
and value type a
in a BST
t
.
The insertion is defined at the value level and the type level.
The returned tree verifies the BST
restrictions.
Instances
Show a => Insertable x a 'EmptyTree Source # | |
(o ~ CmpNat x n, Insertable' x a ('ForkTree l (Node n a1) r) o) => Insertable x a ('ForkTree l (Node n a1) r) Source # | |
class Insertable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where Source #
This type class provides the functionality to insert a node with key x
and value type a
in a non empty BST
t
.
It's only used by the Insertable
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 insertion.
class ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where Source #
class ProofGtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where Source #