
  0 | module TrieOfTrees
  1 | 
  2 | import Data.Maybe
  3 | 
  4 | import FiniteMap
  5 | 
  6 | %default total
  7 | 
  8 | export
  9 | data Tree a = E | T a (Tree a) (Tree a)
 10 | 
 11 | export
 12 | partial
 13 | data Trie : (Type -> Type) -> Type -> Type -> Type where
 14 |   MkTrie : Maybe a -> mk (Trie mk ks (Trie mk ks a)) -> Trie mk ks a
 15 | 
 16 | export
 17 | partial
 18 | {m : Type -> Type -> Type} -> {k : Type} ->
 19 | FiniteMap m k => FiniteMap (Trie (m k)) (Tree k) where
 20 |   empty = MkTrie Nothing empty
 21 | 
 22 |   lookup E t = case t of
 23 |     MkTrie v mk => v
 24 |   lookup (T k a b) t = case t of
 25 |     MkTrie v mk => do
 26 |       m' <- lookup k mk
 27 |       m'' <- lookup a m'
 28 |       lookup b m''
 29 | 
 30 |   bind E x t = case t of
 31 |     MkTrie v mk => MkTrie (Just x) mk
 32 |   bind (T k a b) x t = case t of
 33 |     MkTrie v mk => let tt  = fromMaybe empty $ lookup k mk
 34 |                        t   = fromMaybe empty $ lookup a tt
 35 |                        t'  = bind b x t
 36 |                        tt' = bind a t' tt
 37 |                    in MkTrie v (bind k tt' mk)
 38 |