module trie where open import bool open import char open import list open import maybe open import product open import string open import unit cal : Set β†’ Set cal A = 𝕃 (char Γ— A) empty-cal : βˆ€{A : Set} β†’ cal A empty-cal = [] cal-lookup : βˆ€ {A : Set} β†’ cal A β†’ char β†’ maybe A cal-lookup [] _ = nothing cal-lookup ((c , a) :: l) c' with c =char c' ... | tt = just a ... | ff = cal-lookup l c' cal-insert : βˆ€ {A : Set} β†’ cal A β†’ char β†’ A β†’ cal A cal-insert [] c a = (c , a) :: [] cal-insert ((c' , a') :: l) c a with c =char c' ... | tt = (c , a) :: l ... | ff = (c' , a') :: (cal-insert l c a) cal-remove : βˆ€ {A : Set} β†’ cal A β†’ char β†’ cal A cal-remove [] _ = [] cal-remove ((c , a) :: l) c' with c =char c' ... | tt = cal-remove l c' ... | ff = (c , a) :: cal-remove l c' cal-add : βˆ€{A : Set} β†’ cal A β†’ char β†’ A β†’ cal A cal-add l c a = (c , a) :: l test-cal-insert = cal-insert (('a' , 1) :: ('b' , 2) :: []) 'b' 20 data trie (A : Set) : Set where Node : maybe A β†’ cal (trie A) β†’ trie A empty-trie : βˆ€{A : Set} β†’ trie A empty-trie = (Node nothing empty-cal) trie-lookup-h : βˆ€{A : Set} β†’ trie A β†’ 𝕃 char β†’ maybe A trie-lookup-h (Node odata ts) (c :: cs) with cal-lookup ts c trie-lookup-h (Node odata ts) (c :: cs) | nothing = nothing trie-lookup-h (Node odata ts) (c :: cs) | just t = trie-lookup-h t cs trie-lookup-h (Node odata ts) [] = odata trie-lookup : βˆ€{A : Set} β†’ trie A β†’ string β†’ maybe A trie-lookup t s = trie-lookup-h t (string-to-𝕃char s) trie-contains : βˆ€{A : Set} β†’ trie A β†’ string β†’ 𝔹 trie-contains t s with trie-lookup t s trie-contains t s | nothing = ff trie-contains t s | just _ = tt trie-insert-h : βˆ€{A : Set} β†’ trie A β†’ 𝕃 char β†’ A β†’ trie A trie-insert-h (Node odata ts) [] x = (Node (just x) ts) trie-insert-h (Node odata ts) (c :: cs) x with cal-lookup ts c trie-insert-h (Node odata ts) (c :: cs) x | just t = (Node odata (cal-insert ts c (trie-insert-h t cs x))) trie-insert-h (Node odata ts) (c :: cs) x | nothing = (Node odata (cal-add ts c (trie-insert-h empty-trie cs x))) trie-insert : βˆ€{A : Set} β†’ trie A β†’ string β†’ A β†’ trie A trie-insert t s x = trie-insert-h t (string-to-𝕃char s) x trie-remove-h : βˆ€{A : Set} β†’ trie A β†’ 𝕃 char β†’ trie A trie-remove-h (Node odata ts) (c :: cs) with cal-lookup ts c trie-remove-h (Node odata ts) (c :: cs) | nothing = Node odata ts trie-remove-h (Node odata ts) (c :: cs) | just t = Node odata (cal-insert ts c (trie-remove-h t cs)) trie-remove-h (Node odata ts) [] = Node nothing ts trie-remove : βˆ€{A : Set} β†’ trie A β†’ string β†’ trie A trie-remove t s = trie-remove-h t (string-to-𝕃char s) trie-map : βˆ€{A B : Set} β†’ (A β†’ B) β†’ trie A β†’ trie B trie-cal-map : βˆ€{A B : Set} β†’ (A β†’ B) β†’ cal (trie A) β†’ cal (trie B) trie-map f (Node x x₁) = Node (maybe-map f x) (trie-cal-map f x₁) trie-cal-map f [] = [] trie-cal-map f ((c , t) :: cs) = (c , trie-map f t) :: trie-cal-map f cs trie-to-string-h : βˆ€{A : Set} β†’ string β†’ (A β†’ string) β†’ trie A β†’ 𝕃 char β†’ string trie-cal-to-string-h : βˆ€{A : Set} β†’ string β†’ (A β†’ string) β†’ cal (trie A) β†’ 𝕃 char β†’ string trie-to-string-h sep d (Node (just x) c) prev-str = (𝕃char-to-string (reverse prev-str)) ^ sep ^ (d x) ^ "\n" ^ (trie-cal-to-string-h sep d c prev-str) trie-to-string-h sep d (Node nothing c) prev-str = trie-cal-to-string-h sep d c prev-str trie-cal-to-string-h sep d [] prev-str = "" trie-cal-to-string-h sep d ((c , t) :: cs) prev-str = (trie-to-string-h sep d t (c :: prev-str)) ^ (trie-cal-to-string-h sep d cs prev-str) {- trie-to-string sep d t returns a string representation of the trie t, where each mapping from string s to data x is printed as s sep d x where sep is a string and d returns a string for any element A of the trie. -} trie-to-string : βˆ€{A : Set} β†’ string β†’ (A β†’ string) β†’ trie A β†’ string trie-to-string sep d t = trie-to-string-h sep d t [] trie-mappings-h : βˆ€{A : Set} β†’ trie A β†’ 𝕃 char β†’ 𝕃 (string Γ— A) trie-cal-mappings-h : βˆ€{A : Set} β†’ cal (trie A) β†’ 𝕃 char β†’ 𝕃 (string Γ— A) trie-mappings-h (Node (just x) c) prev-str = (𝕃char-to-string (reverse prev-str) , x) :: (trie-cal-mappings-h c prev-str) trie-mappings-h (Node nothing c) prev-str = (trie-cal-mappings-h c prev-str) trie-cal-mappings-h [] prev-str = [] trie-cal-mappings-h ((c , t) :: cs) prev-str = trie-mappings-h t (c :: prev-str) ++ (trie-cal-mappings-h cs prev-str) trie-mappings : βˆ€{A : Set} β†’ trie A β†’ 𝕃 (string Γ— A) trie-mappings t = trie-mappings-h t [] -- return a list of all the strings which have associated data in the trie trie-strings : βˆ€{A : Set} β†’ trie A β†’ 𝕃 string trie-strings t = map fst (trie-mappings t) trie-nonempty : βˆ€{A : Set} β†’ trie A β†’ 𝔹 trie-cal-nonempty : βˆ€{A : Set} β†’ cal (trie A) β†’ 𝔹 trie-nonempty (Node (just x) t) = tt trie-nonempty (Node nothing c) = trie-cal-nonempty c trie-cal-nonempty [] = ff trie-cal-nonempty ((a , t) :: c) = trie-nonempty t || trie-cal-nonempty c ---------------------------------------------------------------------- -- list-tries, which map strings to lists of values ---------------------------------------------------------------------- 𝕃trie : Set β†’ Set 𝕃trie A = trie (𝕃 A) 𝕃trie-lookup : βˆ€{A : Set} β†’ 𝕃trie A β†’ string β†’ 𝕃 A 𝕃trie-lookup t s with trie-lookup t s ... | nothing = [] ... | just l = l 𝕃trie-add : βˆ€{A : Set} β†’ trie (𝕃 A) β†’ string β†’ A β†’ trie (𝕃 A) 𝕃trie-add t s a = trie-insert t s (a :: 𝕃trie-lookup t s) 𝕃trie-add* : βˆ€{A : Set} β†’ trie (𝕃 A) β†’ string β†’ 𝕃 A β†’ trie (𝕃 A) 𝕃trie-add* t s aa = trie-insert t s (aa ++ 𝕃trie-lookup t s) ---------------------------------------------------------------------- -- stringset ---------------------------------------------------------------------- stringset : Set stringset = trie ⊀ stringset-contains : stringset β†’ string β†’ 𝔹 stringset-contains ss s = trie-contains ss s stringset-insert : stringset β†’ string β†’ stringset stringset-insert ss s = trie-insert ss s triv stringset-remove : stringset β†’ string β†’ stringset stringset-remove ss s = trie-remove ss s stringset-insert𝕃 : stringset β†’ 𝕃 char β†’ stringset stringset-insert𝕃 ss s = trie-insert-h ss s triv empty-stringset : stringset empty-stringset = empty-trie stringset-insert* : stringset β†’ 𝕃 string β†’ stringset stringset-insert* s [] = s stringset-insert* s (x :: xs) = stringset-insert (stringset-insert* s xs) x stringset-strings : βˆ€{A : Set} β†’ trie A β†’ 𝕃 string stringset-strings t = map fst (trie-mappings t)