module Data.Type.List.Map where
import Data.Type.List.List
import Data.Type.List.Proof.Append (Append(..))
import Data.Type.List.Proof.Member (Member(..))
import Data.Proxy (Proxy(..))
data MapC f c where
Nil :: MapC f Nil
(:>) :: MapC f c -> f a -> MapC f (c :> a)
empty :: MapC f Nil
empty = Nil
singleton :: f a -> MapC f (Nil :> a)
singleton x = Nil :> x
lookup :: Member c a -> MapC f c -> f a
lookup Member_Base (_ :> x) = x
lookup (Member_Step mem') (mc :> _) = Data.Type.List.Map.lookup mem' mc
lookup _ _ = error "Should not happen! (Map.lookup)"
mapC :: (forall x. f x -> g x) -> MapC f c -> MapC g c
mapC _ Nil = Nil
mapC f (mc :> x) = mapC f mc :> f x
mapC2 :: (forall x. f x -> g x -> h x) -> MapC f c -> MapC g c -> MapC h c
mapC2 _ Nil Nil = Nil
mapC2 f (xs :> x) (ys :> y) = mapC2 f xs ys :> f x y
append :: MapC f c1 -> MapC f c2 -> MapC f (c1 :++: c2)
append mc Nil = mc
append mc1 (mc2 :> x) = append mc1 mc2 :> x
mkAppend :: MapC f c2 -> Append c1 c2 (c1 :++: c2)
mkAppend Nil = Append_Base
mkAppend (c :> _) = Append_Step (mkAppend c)
mkMonoAppend :: Proxy c1 -> MapC f c2 -> Append c1 c2 (c1 :++: c2)
mkMonoAppend _ = mkAppend
split :: Append c1 c2 c -> MapC f c -> (MapC f c1, MapC f c2)
split Append_Base mc = (mc, Nil)
split (Append_Step app) (mc :> x) = (mc1, mc2 :> x)
where (mc1, mc2) = split app mc
split _ _ = error "Should not happen! (Map.split)"
proxy :: MapC f c -> Proxy c
proxy _ = Proxy
members :: MapC f c -> MapC (Member c) c
members Nil = Nil
members (c :> _) =
mapC Member_Step (members c) :> Member_Base
replace :: MapC f c -> Member c a -> f a -> MapC f c
replace (xs :> _) Member_Base y = xs :> y
replace (xs :> x) (Member_Step memb) y = replace xs memb y :> x