git.iko.soy/Idris-dev
on c79fb21 help sign in
Idris-dev/src/Idris/Core/TC.hs
37 lines 829 B history raw
1{-# LANGUAGE DeriveFunctor #-}
3module Idris.Core.TC(TC'(..)) where
5import Control.Applicative
6import Control.Monad
7import Control.Monad.Trans.Error(Error(..))
9data TC' e a = OK !a
10 | Error e
11 deriving (Eq, Functor)
13bindTC :: TC' e a -> (a -> TC' e b) -> TC' e b
14bindTC x k = case x of
15 OK v -> k v
16 Error e -> Error e
17{-# INLINE bindTC #-}
19instance Error e => Monad (TC' e) where
20 return x = OK x
21 x >>= k = bindTC x k
22 fail e = Error (strMsg e)
24instance Error e => MonadPlus (TC' e) where
25 mzero = fail "Unknown error"
26 (OK x) `mplus` _ = OK x
27 _ `mplus` (OK y) = OK y
28 err `mplus` _ = err
31instance Error e => Applicative (TC' e) where
32 pure = return
33 (<*>) = ap
35instance Error e => Alternative (TC' e) where
36 empty = mzero
37 (<|>) = mplus