{-# OPTIONS --cubical-compatible --safe #-}
module Reflection.TCM.Effectful where
open import Effect.Functor
open import Effect.Applicative
open import Effect.Monad
open import Data.List.Base using ([])
open import Function.Base using (_∘_)
open import Level
open import Reflection.TCM
private
variable
ℓ : Level
functor : RawFunctor {ℓ} TC
functor = record
{ _<$>_ = λ f mx → bindTC mx (return ∘ f)
}
applicative : RawApplicative {ℓ} TC
applicative = record
{ pure = return
; _⊛_ = λ mf mx → bindTC mf λ f → bindTC mx (return ∘ f)
}
applicativeZero : RawApplicativeZero {ℓ} TC
applicativeZero = record
{ applicative = applicative
; ∅ = typeError []
}
alternative : RawAlternative {ℓ} TC
alternative = record
{ applicativeZero = applicativeZero
; _∣_ = catchTC
}
monad : RawMonad {ℓ} TC
monad = record
{ return = return
; _>>=_ = bindTC
}
monadZero : RawMonadZero {ℓ} TC
monadZero = record
{ monad = monad
; applicativeZero = applicativeZero
}
monadPlus : RawMonadPlus {ℓ} TC
monadPlus = record
{ monad = monad
; alternative = alternative
}