Data.OrdPSQ.Internal

(source)

Ordered Priority Search Queue Internals

Definitions

Size : Type

Totality: total
Visibility: public export

data Elem : Type -> Type -> Type -> Type

  Elem k p v binds the key k to the value v with priority p.

Totality: total
Visibility: public export
Constructor:

MkElem : k -> p -> v -> Elem k p v

Hints:

Eq k => Eq p => Eq v => Eq (Elem k p v)
Foldable (Elem k p)
Functor (Elem k p)
Ord k => Ord p => Ord v => Ord (Elem k p v)
Show k => Show p => Show v => Show (Elem k p v)

foldr : (a -> b -> b) -> b -> Elem k p a -> b

Totality: total
Visibility: export

foldl : (b -> a -> b) -> b -> Elem k p a -> b

Totality: total
Visibility: export

map : (a -> b) -> Elem k p a -> Elem k p b

Totality: total
Visibility: export

data LTree : Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Start : LTree k p v
LLoser : Size -> Elem k p v -> LTree k p v -> k -> LTree k p v -> LTree k p v
RLoser : Size -> Elem k p v -> LTree k p v -> k -> LTree k p v -> LTree k p v

Hints:

Eq k => Eq p => Eq v => Eq (LTree k p v)
Foldable (LTree k p)
Functor (LTree k p)
Ord k => Ord p => Ord v => Ord (LTree k p v)
Show k => Show p => Show v => Show (LTree k p v)

foldr : (a -> b -> b) -> b -> LTree k p a -> b

Totality: total
Visibility: export

foldl : (b -> a -> b) -> b -> LTree k p a -> b

Totality: total
Visibility: export

map : (a -> b) -> LTree k p a -> LTree k p b

Totality: total
Visibility: export

data OrdPSQ : Type -> Type -> Type -> Type

  An OrdPSQ uses the Ord instance of the key type to build a priority search queue.
  It is a mapping from keys k to priorities p and values v.

Totality: total
Visibility: public export
Constructors:

Void : OrdPSQ k p v
Winner : Elem k p v -> LTree k p v -> k -> OrdPSQ k p v

Hints:

Eq k => Eq p => Eq v => Eq (OrdPSQ k p v)
Foldable (OrdPSQ k p)
Functor (OrdPSQ k p)
Ord k => Ord p => Ord v => Ord (OrdPSQ k p v)
Show k => Show p => Show v => Show (OrdPSQ k p v)

size' : LTree p k v -> Size

Totality: total
Visibility: export

maxKey : OrdPSQ k p v -> k

Totality: total
Visibility: export

data TourView : Type -> Type -> Type -> Type

Totality: total
Visibility: public export
Constructors:

Null : TourView k p v
Single : Elem k p v -> TourView k p v
Play : OrdPSQ k p v -> OrdPSQ k p v -> TourView k p v

Hints:

Eq k => Eq p => Eq v => Eq (TourView k p v)
Ord k => Ord p => Ord v => Ord (TourView k p v)
Show k => Show p => Show v => Show (TourView k p v)

tourView : OrdPSQ k p v -> TourView k p v

Totality: total
Visibility: export

play : Ord k => Ord p => OrdPSQ k p v -> OrdPSQ k p v -> OrdPSQ k p v

  Take two pennants and returns a new pennant that is the union of
  the two with the precondition that the keys in the first tree are
  strictly smaller than the keys in the second tree.

Totality: total
Visibility: export