Accompanying material for the paper "Generalizing Generalized Tries"
by Ralf Hinze, in Journal of Functional Programming, 10(4),
pp. 327-351, July 2000.

Spotted tries for de Bruijn terms of type `Term v'.

> module MapTerm (
>     MapT,
>     showMapT,
>     emptyT,
>     singleT,
>     lookupT,
>     mergeT,
> ) where
> import Term
> import Map (showMaybe, (<>), combine)
> import MapIncr

> data MapT m v			=  SpotT
>				|  TrieT (m v)
>				         (MapT m (MapT m v))
>				         (MapT (MapI m) v)

> showMapT			:: (forall v.(Int -> v -> ShowS) -> (Int -> m v -> ShowS))
>				   -> (Int -> w -> ShowS) -> (Int -> MapT m w -> ShowS)
> showMapT showm showw d SpotT	=  showString "SpotT"
> showMapT showm showw d (TrieT tv ta tl)
>				=  showParen (d >= 10) (
>				       showString "TrieT " . showm showw 10 tv
>				           . showChar ' ' . showMapT showm (showMapT showm showw) 10 ta
>				           . showChar ' ' . showMapT (showMapI showm) showw 10 tl)

> emptyT			:: MapT m w
> emptyT			=  SpotT

> singleT			:: (forall v.m v) -> (forall v.(k, v) -> m v)
>				   -> ((Term k, w) -> MapT m w)
> singleT e s (Var i, v)	=  TrieT (s (i, v)) emptyT emptyT
> singleT e s (App i1 i2, v)	=  TrieT e (singleT e s (i1, singleT e s (i2, v))) emptyT
> singleT e s (Lam i, v)	=  TrieT e emptyT (singleT emptyI (singleI e s) (i, v))

> lookupT			:: (forall v.k -> m v -> Maybe v)
>				   -> (Term k -> MapT m w -> Maybe w)
> lookupT l i SpotT		=  Nothing
> lookupT l (Var i) (TrieT tv ta tl)
>				=  l i tv
> lookupT l (App i1 i2) (TrieT tv ta tl)
>				=  (lookupT l i1 <> lookupT l i2) ta
> lookupT l (Lam i) (TrieT tv ta tl)
>				=  lookupT (lookupI l) i tl

> mergeT			:: (forall v.(v -> v -> v) -> (m v -> m v -> m v))
>				   -> ((w -> w -> w)
>				       -> (MapT m w -> MapT m w -> MapT m w))
> mergeT m c SpotT t'		=  t'
> mergeT m c t SpotT		=  t
> mergeT m c (TrieT tv ta tl) (TrieT tv' ta' tl')
>				=  TrieT (m c tv tv')
>				         (mergeT m (mergeT m c) ta ta')
>				         (mergeT (mergeI m) c tl tl')