Agda.Utils.Trie

Strict tries (based on Strict and Strict).

Documentation

data Trie k v

Finite map from [k] to v.

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

Instances

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

empty :: Trie k v

Empty trie.

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

Singleton trie.

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

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

Insert with function merging new value with old value.

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

Left biased union.

union = unionWith ( new old -> new).

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

Pointwise union with merge function for values.

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

Adjust value at key, leave subtree intact.

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

Delete value at key, but leave subtree intact.

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

Convert to ascending list.

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

Convert to ascending list.

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

Collect all values along a given path.