{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}

module Control.IxMonad.Reader (HNil'(..), HCons'(..), ask, Split(..)) where

import Control.IxMonad
import Control.IxMonad.Cond
import Data.HList hiding (Monad(..))
import Prelude    hiding (Monad(..))

instance IxMonad (->) where
    type Inv (->) s t = Split s t

    type Unit (->) = HNil'
    type Plus (->) s t = Append s t

    return x = \HNil' -> x
    e >>= k = \xs -> let (s, t) = split xs
                     in (k (e s)) t

ask :: (HCons' a HNil') -> a
ask = \(HCons' a HNil') -> a

-- Type-level append, and dual operations for split

class Split s t where
    type Append s t
    split :: Append s t -> (s, t)

instance Split HNil' t where
    type Append HNil' t = t
    split t = (HNil', t)

instance Split xs ys => Split (HCons' x xs) ys where
    type Append (HCons' x xs) ys = HCons' x (Append xs ys)
    split (HCons' x xs) = let (xs', ys') = split xs
                         in (HCons' x xs', ys')

-- Conditionals

instance Cond (->) where
    type AltInv (->) s t = Split s t
    type Alt (->) s t = Append s t

    ifM True x y = \rs -> let (r, s) = split rs
                              _      = y s 
                          in x r
    ifM False x y = \rs -> let (r, s) = split rs
                               _      = x r 
                           in y s