git.iko.soy/Idris-dev
on dd09721 help sign in
Idris-dev/src/Idris/Core/TC.hs
28 lines 639 B history raw
1{-# LANGUAGE DeriveFunctor #-}
3module Idris.Core.TC(TC'(..)) where
5import Control.Monad
6import Control.Monad.Trans.Error(Error(..))
8data TC' e a = OK !a
9 | Error e
10 deriving (Eq, Functor)
12bindTC :: TC' e a -> (a -> TC' e b) -> TC' e b
13bindTC x k = case x of
14 OK v -> k v
15 Error e -> Error e
16{-# INLINE bindTC #-}
18instance Error e => Monad (TC' e) where
19 return x = OK x
20 x >>= k = bindTC x k
21 fail e = Error (strMsg e)
23instance Error e => MonadPlus (TC' e) where
24 mzero = fail "Unknown error"
25 (OK x) `mplus` _ = OK x
26 _ `mplus` (OK y) = OK y
27 err `mplus` _ = err