------------------------------------------------------------------------
-- The Agda standard library
--
-- Trie, basic type and operations
------------------------------------------------------------------------
-- See README.Data.Trie.NonDependent for an example of using a trie to
-- build a lexer.
{-# OPTIONS --cubical-compatible --sized-types #-}
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (StrictTotalOrder)
module Data.Trie {k e r} (S : StrictTotalOrder k e r) where
open import Level
open import Size
open import Data.List.Base using (List; []; _∷_; _++_)
import Data.List.NonEmpty as List⁺
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe′)
open import Data.Product.Base using (∃)
open import Data.These.Base as These using (These)
open import Function.Base using (_∘′_; const)
open import Relation.Unary using (IUniversal; _⇒_)
open StrictTotalOrder S
using (module Eq)
renaming (Carrier to Key)
open import Data.List.Relation.Binary.Equality.Setoid Eq.setoid
open import Data.Tree.AVL.Value ≋-setoid using (Value)
------------------------------------------------------------------------
-- Definition
-- Trie is defined in terms of Trie⁺, the type of non-empty trie. This
-- guarantees that the trie is minimal: each path in the tree leads to
-- either a value or a number of non-empty sub-tries.
open import Data.Trie.NonEmpty S as Trie⁺ public
using (Trie⁺; Tries⁺; Word; eat)
Trie : ∀ {v} (V : Value v) → Size → Set (v ⊔ k ⊔ e ⊔ r)
Trie V i = Maybe (Trie⁺ V i)
------------------------------------------------------------------------
-- Operations
-- Functions acting on Trie are wrappers for functions acting on Tries.
-- Sometimes the empty case is handled in a special way (e.g. insertWith
-- calls singleton when faced with an empty Trie).
module _ {v} {V : Value v} where
private Val = Value.family V
------------------------------------------------------------------------
-- Lookup
lookup : Trie V ∞ → ∀ ks → Maybe (These (Val ks) (Tries⁺ (eat V ks) ∞))
lookup t ks = t Maybe.>>= λ ts → Trie⁺.lookup ts ks
lookupValue : Trie V ∞ → ∀ ks → Maybe (Val ks)
lookupValue t ks = t Maybe.>>= λ ts → Trie⁺.lookupValue ts ks
lookupTries⁺ : Trie V ∞ → ∀ ks → Maybe (Tries⁺ (eat V ks) ∞)
lookupTries⁺ t ks = t Maybe.>>= λ ts → Trie⁺.lookupTries⁺ ts ks
lookupTrie : Trie V ∞ → ∀ k → Trie (eat V (k ∷ [])) ∞
lookupTrie t k = t Maybe.>>= λ ts → Trie⁺.lookupTrie⁺ ts k
------------------------------------------------------------------------
-- Construction
empty : Trie V ∞
empty = nothing
singleton : ∀ ks → Val ks → Trie V ∞
singleton ks v = just (Trie⁺.singleton ks v)
insertWith : ∀ ks → (Maybe (Val ks) → Val ks) → Trie V ∞ → Trie V ∞
insertWith ks f (just t) = just (Trie⁺.insertWith ks f t)
insertWith ks f nothing = singleton ks (f nothing)
insert : ∀ ks → Val ks → Trie V ∞ → Trie V ∞
insert ks = insertWith ks ∘′ const
fromList : List (∃ Val) → Trie V ∞
fromList = Maybe.map Trie⁺.fromList⁺ ∘′ List⁺.fromList
toList : Trie V ∞ → List (∃ Val)
toList (just t) = List⁺.toList (Trie⁺.toList⁺ t)
toList nothing = []
------------------------------------------------------------------------
-- Modification
module _ {v w} {V : Value v} {W : Value w} where
private
Val = Value.family V
Wal = Value.family W
map : ∀ {i} → ∀[ Val ⇒ Wal ] → Trie V i → Trie W i
map = Maybe.map ∘′ Trie⁺.map V W
-- Deletion
module _ {v} {V : Value v} where
-- Use a function to decide how to modify the sub-Trie⁺ whose root is
-- at the end of path ks.
deleteWith : ∀ {i} (ks : Word) →
(∀ {i} → Trie⁺ (eat V ks) i → Maybe (Trie⁺ (eat V ks) i)) →
Trie V i → Trie V i
deleteWith ks f t = t Maybe.>>= Trie⁺.deleteWith ks f
-- Remove the whole node
deleteTrie⁺ : ∀ {i} (ks : Word) → Trie V i → Trie V i
deleteTrie⁺ ks t = t Maybe.>>= Trie⁺.deleteTrie⁺ ks
-- Remove the value and keep the sub-Tries (if any)
deleteValue : ∀ {i} (ks : Word) → Trie V i → Trie V i
deleteValue ks t = t Maybe.>>= Trie⁺.deleteValue ks
-- Remove the sub-Tries and keep the value (if any)
deleteTries⁺ : ∀ {i} (ks : Word) → Trie V i → Trie V i
deleteTries⁺ ks t = t Maybe.>>= Trie⁺.deleteTries⁺ ks
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4