Agda-2.8.0: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Trie

Description

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

Documentation

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

Instances

Instances details
Foldable (Trie k) Source # 
Instance details

Defined in Agda.Utils.Trie

Methods

fold :: Monoid m => Trie k m -> m #

foldMap :: Monoid m => (a -> m) -> Trie k a -> m #

foldMap' :: Monoid m => (a -> m) -> Trie k a -> m #

foldr :: (a -> b -> b) -> b -> Trie k a -> b #

foldr' :: (a -> b -> b) -> b -> Trie k a -> b #

foldl :: (b -> a -> b) -> b -> Trie k a -> b #

foldl' :: (b -> a -> b) -> b -> Trie k a -> b #

foldr1 :: (a -> a -> a) -> Trie k a -> a #

foldl1 :: (a -> a -> a) -> Trie k a -> a #

toList :: Trie k a -> [a] #

null :: Trie k a -> Bool #

length :: Trie k a -> Int #

elem :: Eq a => a -> Trie k a -> Bool #

maximum :: Ord a => Trie k a -> a #

minimum :: Ord a => Trie k a -> a #

sum :: Num a => Trie k a -> a #

product :: Num a => Trie k a -> a #

Functor (Trie k) Source # 
Instance details

Defined in Agda.Utils.Trie

Methods

fmap :: (a -> b) -> Trie k a -> Trie k b #

(<$) :: a -> Trie k b -> Trie k a #

(Ord a, EmbPrj a, EmbPrj b) => EmbPrj (Trie a b) Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Trie a b -> S Word32 Source #

icod_ :: Trie a b -> S Word32 Source #

value :: Word32 -> R (Trie a b) Source #

Null (Trie k v) Source #

Empty trie.

Instance details

Defined in Agda.Utils.Trie

Methods

empty :: Trie k v Source #

null :: Trie k v -> Bool Source #

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

Defined in Agda.Utils.Trie

Methods

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

show :: Trie k v -> String #

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

(NFData k, NFData v) => NFData (Trie k v) Source # 
Instance details

Defined in Agda.Utils.Trie

Methods

rnf :: Trie k v -> () #

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

Defined in Agda.Utils.Trie

Methods

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

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

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.

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

delete :: 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.

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.

toListOrderedBy :: 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.

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.

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

Get the subtrie rooted at the given key.

mapSubTries :: 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.

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

Filter a trie.

valueAt :: Ord k => [k] -> Lens' (Trie k v) (Maybe v) Source #

Key lens.