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

{- |

Module      :  Data.Yoko.Reduce
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

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

Reduction of a band of constructors into a mediation of their range.

-}
module Data.Yoko.Reduce (AnRMNUni, Reduce(..), ReduceDC(..)) where

import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.Reflect



type AnRMNUni m ts = AnRMN m (Uni ts)



-- | @reduce@ embeds a mediated sum of constructors into a mediation of their
-- range.
class (dcs ::: All IsDC) => Reduce m dcs where
  reduce :: AnRMNUni m dcs -> Med m (LeftmostRange dcs)

instance (Med m (LeftmostRange ts) ~ Med m (LeftmostRange us),
          Reduce m ts, Reduce m us) => Reduce m (ts :+ us) where
  reduce = reduce `two` reduce
instance ReduceDC m dc => Reduce m (N dc) where
  reduce = reduceDC . unRMNUni where
    unRMNUni :: AnRMNUni m (N dc) -> RMN m dc
    unRMNUni (NP (Uni (Here Refl)) x) = x

-- | @reduceDC@ embeds a mediated constructor into a mediation of its range.
class DC dc => ReduceDC m dc where reduceDC :: RMN m dc -> Med m (Range dc)



type OneOf ts = NP (Uni ts)

two :: (OneOf ts f -> a) -> (OneOf us f -> a) -> (OneOf (ts :+ us) f -> a)
two f g (NP (Uni tag) x) = case tag of
  OnLeft u -> f $ NP (Uni u) x
  OnRight v -> g $ NP (Uni v) x