module Type.Yoko.BTree where
import Type.Yoko.Type
import Type.Yoko.Universe
import Type.Yoko.Natural
import Data.Yoko.Core
import Type.Yoko.Sum
type Inu t = Exists ((:=:) t)
newtype Uni ts t = Uni (Inu t ts)
instance (ts ::: Inu t) => t ::: Uni ts where inhabits = Uni inhabits
type instance Pred (Uni ts) t = Elem t ts
instance (ts ::: TSum) => EqT (Uni ts) where
eqT (Uni u) (Uni v) = w u v where
w :: forall ts a b. Inu a ts -> Inu b ts -> Maybe (a :=: b)
w (Here Refl) (Here Refl) = Just Refl
w (OnLeft u) (OnLeft v) = w u v
w (OnRight u) (OnRight v) = w u v
w _ _ = Nothing
type family PrimUni ts :: * -> *
type instance PrimUni V = VoidU
type instance PrimUni (N t) = (:=:) t
type instance PrimUni (ts :+ us) = PrimUni ts :|| PrimUni us
primUni :: Uni ts t -> PrimUni ts t
primUni (Uni u) = w u where
w :: Inu t ts -> PrimUni ts t
w (Here Refl) = Refl
w (OnLeft u) = LeftD $ w u
w (OnRight v) = RightD $ w v
primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t
primUni1 (Uni (OnLeft u)) = LeftD $ Uni u
primUni1 (Uni (OnRight v)) = RightD $ Uni v
type family Inhabitants u
class (Inhabitants u ::: TSum) => Finite u where
toUni :: u t -> Uni (Inhabitants u) t
class Finite u => Etinif u where fromUni :: Uni (Inhabitants u) t -> u t
eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v
) => u a -> v b -> Maybe (a :=: b)
eqTFin x y = eqT (toUni x) (toUni y)
type instance Inhabitants (Uni ts) = ts
instance (ts ::: TSum) => Finite (Uni ts) where toUni = id
instance Finite (Uni ts) => Etinif (Uni ts) where fromUni = id
type family Norm c
type instance Norm V = V
type instance Norm (N t) = N t
type instance Norm (ts :+ us) = NormW (ts :+ us) V
type family NormW c acc
type instance NormW V acc = acc
type instance NormW (N t) acc = If (Elem t acc) acc (N t :+ acc)
type instance NormW (ts :+ us) acc = NormW ts (NormW us acc)
type Each ts = NT (Uni ts)
none :: String -> Each V f
none s = NT $ error $ "TypeBTree.none: " ++ s
one_ :: [qP|f :: *->*|] -> Unwrap f t -> Each (N t) f
one_ p x = firstNT primUni $ constNT_ p x
one :: Unwrap f t -> Each (N t) f
one = one_ Proxy
oneF :: Wrapper f => f t -> Each (N t) f
oneF x = firstNT primUni $ constNTF x
infixr 6 |||, .|.
both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) f
both f g = firstNT primUni1 $ orNT f g; (|||) = both
infixl 5 ||.; infixr 5 .||
(.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) f
(||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) f
(.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) f
f .|. g = one f ||| one g; f ||. g = f ||| one g; f .|| g = one f ||| g
each :: forall u ts f. (ts ::: All u) => [qP|u :: *->*|] ->
(forall a. u a -> Unwrap f a) -> Each ts f
each _ = \fs -> w inhabits fs where
w :: forall ts. All u ts ->
(forall a. (a ::: u) => u a -> Unwrap f a) -> Each ts f
w SumV _ = none "TypeBTree.each"
w (SumN u) fns = one $ fns u
w (SumS c d) fns = w c fns `both` w d fns
eachF :: forall u ts f. (Wrapper f, ts ::: All u) => [qP|u :: *->*|] ->
(forall a. u a -> f a) -> Each ts f
eachF p f = each p (unwrap . f)
eachF_ :: forall f ts. (Wrapper f, ts ::: All NoneD) => (forall a. f a) -> Each ts f
eachF_ f = eachF Proxy ((\NoneD -> f) :: forall a. NoneD a -> f a)
prjEach :: Uni ts t -> Each ts f -> Unwrap f t
prjEach x f = appNT f x
prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f t
prjEachF = (wrap .) . prjEach
eachOrNT :: forall u v f w.
(Inhabitants v ::: All (u :|| w), Finite v) => NT u f -> NT w f -> NT v f
eachOrNT fs dflt = firstNT toUni $ each Proxy $ appNT $ orNT fs dflt