------------------------------------------------------------------------
-- The Agda standard library
--
-- Typeclass instances for TC
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Reflection.TCM.Effectful where

open import Effect.Choice
open import Effect.Empty
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 (pure ∘ f)
  }

applicative : RawApplicative {ℓ} TC
applicative = record
  { rawFunctor = functor
  ; pure = pure
  ; _<*>_  = λ mf mx → bindTC mf λ f → bindTC mx (pure ∘ f)
  }

empty : RawEmpty {ℓ} TC
empty = record { empty = typeError [] }

applicativeZero : RawApplicativeZero {ℓ} TC
applicativeZero = record
  { rawApplicative = applicative
  ; rawEmpty = empty
  }

choice : RawChoice {ℓ} TC
choice = record { _<|>_ = catchTC }

alternative : RawAlternative {ℓ} TC
alternative = record
  { rawApplicativeZero = applicativeZero
  ; rawChoice = choice
  }

monad : RawMonad {ℓ} TC
monad = record
  { rawApplicative = applicative
  ; _>>=_  = bindTC
  }

monadZero : RawMonadZero {ℓ} TC
monadZero = record
  { rawMonad = monad
  ; rawEmpty = empty
  }

monadPlus : RawMonadPlus {ℓ} TC
monadPlus = record
  { rawMonadZero = monadZero
  ; rawChoice = choice
  }