Agda-2.5.1.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Utils.Trie

Description

Strict tries (based on Data.Map.Strict and Agda.Utils.Maybe.Strict).

Synopsis

Documentation

data Trie k v Source #

Finite map from [k] to v.

With the strict Maybe type, Trie is also strict in v.

Instances

(Eq k, Eq v) => Eq (Trie k v) Source # 

Methods

(==) :: Trie k v -> Trie k v -> Bool #

(/=) :: Trie k v -> Trie k v -> Bool #

(Show k, Show v) => Show (Trie k v) Source # 

Methods

showsPrec :: Int -> Trie k v -> ShowS #

show :: Trie k v -> String #

showList :: [Trie k v] -> ShowS #

Null (Trie k v) Source #

Empty trie.

Methods

empty :: Trie k v Source #

null :: Trie k v -> Bool Source #

empty :: Null a => a Source #

singleton :: [k] -> v -> Trie k v Source #

Singleton trie.

everyPrefix :: [k] -> v -> Trie k v Source #

everyPrefix k v is a trie where every prefix of k (including k itself) is mapped to v.

insert :: Ord k => [k] -> v -> Trie k v -> Trie k v Source #

Insert. Overwrites existing value if present.

insert = insertWith ( new old -> new)

insertWith :: Ord k => (v -> v -> v) -> [k] -> v -> Trie k v -> Trie k v Source #

Insert with function merging new value with old value.

union :: Ord k => Trie k v -> Trie k v -> Trie k v Source #

Left biased union.

union = unionWith ( new old -> new).

unionWith :: Ord k => (v -> v -> v) -> Trie k v -> Trie k v -> Trie k v Source #

Pointwise union with merge function for values.

adjust :: Ord k => [k] -> (Maybe v -> Maybe v) -> Trie k v -> Trie k v Source #

Adjust value at key, leave subtree intact.

delete :: Ord k => [k] -> Trie k v -> Trie k v Source #

Delete value at key, but leave subtree intact.

toList :: Ord k => Trie k v -> [([k], v)] Source #

Convert to ascending list.

toAscList :: Ord k => Trie k v -> [([k], v)] Source #

Convert to ascending list.

lookup :: Ord k => [k] -> Trie k v -> Maybe v Source #

Returns the value associated with the given key, if any.

member :: Ord k => [k] -> Trie k v -> Bool Source #

Is the given key present in the trie?

lookupPath :: Ord k => [k] -> Trie k v -> [v] Source #

Collect all values along a given path.

tests :: IO Bool Source #

All tests.