HORIZON HASKELLDocslts/ghc-9.14.x3e2d5682026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · 3e2d568 · 2026-10-11

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).

  • 1 type
  • 18 values
  • PackageAgda-2.8.0.2
  • Exports20
  • LanguageHaskell2010
  • LicenceMIT
  • SourceTrie.hs
datadata Trie k v
#

Finite map from [k] to v.

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

Constructors

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
valueeveryPrefix :: [k] -> v -> Trie k v
#

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
#

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
#

Insert with function merging new value with old value.

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

Left biased union.

union = unionWith ( new old -> new).

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

Pointwise union with merge function for values.

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

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
#

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)]
#

Convert to ascending list.

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

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
#

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

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

Is the given key present in the trie?

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

Collect all values along a given path.

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

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