
  0 | module Trie
  1 | 
  2 | import Data.Maybe
  3 | 
  4 | import FiniteMap
  5 | 
  6 | %default total
  7 | 
  8 | export
  9 | partial
 10 | data Trie : (Type -> Type) -> Type -> Type -> Type where
 11 |   MkTrie : Maybe a -> mk (Trie mk ks a) -> Trie mk ks a
 12 | 
 13 | export
 14 | partial
 15 | {m : Type -> Type -> Type} -> {k : Type} ->
 16 | FiniteMap m k => FiniteMap (Trie (m k)) (List k) where
 17 |   empty = MkTrie Nothing empty
 18 | 
 19 |   lookup [] t = case t of
 20 |     MkTrie b m => b
 21 |   lookup (k :: ks) t = case t of
 22 |     MkTrie b m => lookup k m >>= \m' => lookup ks m'
 23 | 
 24 |   bind [] x t = case t of
 25 |     MkTrie b m => MkTrie (Just x) m
 26 |   bind (k :: ks) x t = case t of
 27 |     MkTrie b m => let t = fromMaybe empty $ lookup k m
 28 |                       t' = bind ks x t
 29 |                   in MkTrie b (bind k t' m)
 30 |