ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Trie

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

Note that if delete or adjust are used, one may end up with non-canonical subtries, i.e., those that do not contain any value (Data.List.null . toList) but may be Eq-different to other empty tries (/= empty).

Synopsis

data Trie
method empty
value singleton
value everyPrefix
value insert
value insertWith
value union
value unionWith
value adjust
value delete
value toList
value toAscList
value toListOrderedBy
value lookup
value member
value lookupPath
value lookupTrie
value mapSubTries
value filter
value valueAt

PackageAgda-2.8.0.2
Exports20
LanguageHaskell2010
LicenceMIT
SourceTrie.hs

datadata Trie k v

Source#

Finite map from [k] to v.

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

Constructors

Trie !(Maybe v) !(Map k (Trie k v))

Instances7Functor, Foldable, Eq, Show, NFData, Null, …

Functor (Trie k)Defined in Agda-2.8.0.2 · Agda.Utils.Trie
Foldable (Trie k)Defined in Agda-2.8.0.2 · Agda.Utils.Trie
(Eq v, Eq k) => Eq (Trie k v)Defined in Agda-2.8.0.2 · Agda.Utils.Trie
(Show v, Show k) => Show (Trie k v)Defined in Agda-2.8.0.2 · Agda.Utils.Trie
(NFData k, NFData v) => NFData (Trie k v)Defined in Agda-2.8.0.2 · Agda.Utils.Trie
Null (Trie k v)Defined in Agda-2.8.0.2 · Agda.Utils.Trie
Empty trie.
(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Serialise.Instances.Common · orphan

methodempty :: a

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

Source#

Singleton trie.

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

Source#

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

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

Source#

Insert. Overwrites existing value if present.

insert = insertWith ( new old -> new)

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

Source#

Insert with function merging new value with old value.

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

Source#

Left biased union.

union = unionWith ( new old -> new).

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

Source#

Pointwise union with merge function for values.

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

Source#

Adjust value at key, leave subtree intact.

Disclaimer: may return a non-canoncial trie because it does not clean up subtries that become empty.

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

Source#

Delete value at key, but leave subtree intact.

Disclaimer: may return a non-canoncial trie because it does not clean up subtries that become empty.

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

Source#

Convert to ascending list.

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

Source#

Convert to ascending list.

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

Source#

Convert to list where nodes at the same level are ordered according to the given ordering.

valuelookup :: Ord k => [k] -> Trie k v -> Maybe v

Source#

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

valuemember :: Ord k => [k] -> Trie k v -> Bool

Source#

Is the given key present in the trie?

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

Source#

Collect all values along a given path.

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

Source#

Get the subtrie rooted at the given key.

valuemapSubTries :: Ord k => (Trie k u -> Maybe v) -> Trie k u -> Trie k v

Source#

Create new values based on the entire subtrie. Almost, but not quite comonad extend.

valuefilter :: Ord k => (v -> Bool) -> Trie k v -> Trie k v

Source#

Filter a trie.

valuevalueAt :: Ord k => [k] -> Lens' (Trie k v) (Maybe v)

Source#

Key lens.