module Idris.Core.TC(TC'(..)) where
import Control.Applicative
import Control.Monad
import Control.Monad.Trans.Error(Error(..))
data TC' e a = OK !a
| Error e
deriving (Eq, Functor)
bindTC :: TC' e a -> (a -> TC' e b) -> TC' e b
bindTC x k = case x of
OK v -> k v
Error e -> Error e
instance Error e => Monad (TC' e) where
return x = OK x
x >>= k = bindTC x k
fail e = Error (strMsg e)
instance Error e => MonadPlus (TC' e) where
mzero = fail "Unknown error"
(OK x) `mplus` _ = OK x
_ `mplus` (OK y) = OK y
err `mplus` _ = err
instance Error e => Applicative (TC' e) where
pure = return
(<*>) = ap
instance Error e => Alternative (TC' e) where
empty = mzero
(<|>) = mplus