{-# LANGUAGE TypeFamilies, ScopedTypeVariables, QuasiQuotes, Rank2Types,
  GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
  UndecidableInstances, EmptyDataDecls, TypeOperators #-}

{-# LANGUAGE TemplateHaskell #-}

{- |

Module      :  Type.Yoko.BTree
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Operators for the type-sums from "Type.Yoko.Sum".

-}

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





-- | @Inu t@ is a universe of type-sums containing @t@.
type Inu t = Exists ((:=:) t)

-- | @Uni ts@ is a universe containing the types in the type-sum @ts@.
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 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 





-- | A @Uni ts t@ value can also be understood in terms of more primitive
-- universes, 'VoidU', @':=:'@ and @':||'@ for 'V', 'N', and @':+'@,
-- respectively.
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) = LeftU $ w u
  w (OnRight v) = RightU $ w v

primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t
primUni1 (Uni (OnLeft u)) = LeftU $ Uni u
primUni1 (Uni (OnRight v)) = RightU $ Uni v




-- | Finite universes can be represented as type-sums.
type family Inhabitants u
class Finite u where
  toUni :: u t -> Uni (Inhabitants u) t

finiteNP :: Finite u => NP u f -> NP (Uni (Inhabitants u)) f
finiteNP = firstNP toUni

-- | @frUni@ sometimes requires a stronger context than does @toUni@, so we
-- separate the two methods.
class Finite u => Etinif u where frUni :: Uni (Inhabitants u) t -> u t

-- | Any finite universe can be used to determine type equality.
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 Finite (Uni ts) where toUni = id
instance Finite (Uni ts) => Etinif (Uni ts) where frUni = id

type instance Inhabitants VoidU = V

type instance Inhabitants ((:=:) t) = N t
instance Finite ((:=:) t) where toUni Refl = Uni (Here Refl)
instance Etinif ((:=:) t) where frUni (Uni (Here Refl)) = Refl

type instance Inhabitants (u :|| v) = Inhabitants u :+ Inhabitants v
instance (Finite u, Finite v) => Finite (u :|| v) where
  toUni (LeftU u) = case toUni u of
    Uni x -> Uni $ OnLeft $ x
  toUni (RightU v) = case toUni v of
    Uni x -> Uni $ OnRight $ x
instance (Etinif u, Etinif v) => Etinif (u :|| v) where
  frUni uv = case primUni1 uv of
    LeftU u -> LeftU $ frUni u
    RightU v -> RightU $ frUni v


-- | @Norm@ uses @NormW@ to remove duplicates from (i.e. /normalize/) a
-- type-sum.
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

-- | @NormW@ combines two type-sums into a right-associated type-sum containing
-- no duplicates.
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)




-- | @Each ts f@ provides a @'NT' t f@ for each @t@ in the type-sum @ts@.
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@ is the principal means of defining an @Each@ value.
each :: forall u v f. (Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->
        (forall a. u a -> Unwrap f a) -> NT v f
each _ = \fs -> firstNT toUni $ 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 v f. (Wrapper f, Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->
         (forall a. u a -> f a) -> NT v f
eachF p f = each p (unwrap . f)

eachF_ :: forall f v. (Wrapper f, Inhabitants v ::: All NoneU, Finite v) => (forall a. f a) -> NT v f
eachF_ f = eachF Proxy ((\NoneU -> f) :: forall a. NoneU a -> f a)



-- | Just a specialization: @prjEach x f = 'appNT' f x@.
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 fs gs@ builds an 'NT' that uses @fs@ for as many types in the
-- universe @v@ as possible, and uses @gs@ for the rest. It's an extension of
-- 'orNT' to @Each@.
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