| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Utils.CompressedTrie
Description
Strict compressed tries (based on Data.Map.Strict and Agda.Utils.Maybe.Strict).
In contrast to Agda.Utils.Trie, branches from a node can be labeled with non-empty lists of keys that do not overlap, meaning they start with different first elements. This way, non-branching unlabelled pathes can be stored more efficiently.
As a side effect, the notion of height changes
which we utilize in the truncate function.
An Trie is usually constructed
from an Trie via the compress function.
Synopsis
- data Trie k v = Trie {}
- root :: v -> Trie k v
- singleton :: [k] -> v -> Trie k v
- singleton1 :: List1 k -> v -> Trie k v
- singleBranch :: List1 k -> Trie k v -> (List1 k, Trie k v)
- isSingleBranch :: Trie k v -> Maybe (List1 k, Trie k v)
- compress :: Ord k => Trie k v -> Trie k v
- uncompress :: Ord k => Trie k v -> Trie k v
- toList :: Ord k => Trie k v -> [([k], v)]
- toAscList :: Ord k => Trie k v -> [([k], v)]
- size :: Trie k v -> Int
- sizeWithLeaves :: Trie k v -> Int
- substLeaves :: (Maybe v -> Trie k v) -> Trie k v -> Trie k v
- truncate :: Int -> Trie k v -> Trie k v
- truncateSize :: (Trie k v -> Int) -> Int -> Trie k v -> Trie k v
- truncateSizeWithLeaves :: Int -> Trie k v -> Trie k v
Documentation
Finite map from [k] to v.
With the strict Maybe type, Trie is also strict in v.
Invariant: only the root of the tree
may be of the form Trie Nothing (Map.singleton ks t).
A node inside of the trie of that form must be fused
into its branch.
Instances
| Functor (Trie k) Source # | |
| Foldable (Trie k) Source # | |
Defined in Agda.Utils.CompressedTrie 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 # elem :: Eq a => a -> Trie k a -> Bool # maximum :: Ord a => Trie k a -> a # minimum :: Ord a => Trie k a -> a # | |
| Null (Trie k v) Source # | Empty trie. |
| (NFData k, NFData v) => NFData (Trie k v) Source # | |
Defined in Agda.Utils.CompressedTrie | |
| (Show v, Show k) => Show (Trie k v) Source # | |
| (Eq v, Eq k) => Eq (Trie k v) Source # | |
| Singleton ([k], v) (Trie k v) Source # | |
Defined in Agda.Utils.CompressedTrie | |
Construction
singleton1 :: List1 k -> v -> Trie k v Source #
Singleton tree with empty root.
singleBranch :: List1 k -> Trie k v -> (List1 k, Trie k v) Source #
A single branch with the given subtree. Precondition: the given subtree has a value at the root.
isSingleBranch :: Trie k v -> Maybe (List1 k, Trie k v) Source #
Is the trie starting with a single branch?
Deconstruction
uncompress :: Ord k => Trie k v -> Trie k v Source #
Turn a compressed trie into an uncompressed trie.
sizeWithLeaves :: Trie k v -> Int Source #
The number of nodes that are labeled or leaves..
Modification
substLeaves :: (Maybe v -> Trie k v) -> Trie k v -> Trie k v Source #
Modify the leaves (input and output may be non-canonical).
truncate :: Int -> Trie k v -> Trie k v Source #
Truncate tree at given depth.
truncate 0 t returns the root.