{-# OPTIONS --safe --without-K #-}
--------------------------------------------------------------------------------
-- Improved TC
--------------------------------------------------------------------------------
 
module Reflection.TCI where
 
open import Meta.Prelude
 
open import Data.List using (map)
 
import Agda.Builtin.Reflection as R'
import Reflection as R
open import Reflection.Syntax
 
open import Class.Monad hiding (Monad-TC)
open import Class.MonadError using (MonadError)
open import Class.MonadReader
open import Class.MonadTC
 
open Monad
 
private variable a f : Level
                 A B C D : Set a
 
TC : Set a → Set a
TC = ReaderT TCEnv R.TC
 
Monad-TC : Monad TC
Monad-TC = Monad-ReaderT ⦃ Class.Monad.Monad-TC ⦄
 
MonadReader-TC : MonadReader TCEnv TC ⦃ Monad-TC ⦄
MonadReader-TC = MonadReader-ReaderT ⦃ Class.Monad.Monad-TC ⦄
 
MonadError-TC : MonadError (List ErrorPart) TC
MonadError-TC = MonadError-ReaderT ⦃ Class.Monad.Monad-TC ⦄ ⦃ Class.MonadError.MonadError-TC ⦄
 
applyReductionOptions : TC A → TC A
applyReductionOptions x r@record { reduction = onlyReduce red } = R'.withReduceDefs (true ,  red) (x r)
applyReductionOptions x r@record { reduction = dontReduce red } = R'.withReduceDefs (false , red) (x r)
 
applyNormalisation : TC A → TC A
applyNormalisation x r@record { normalisation = n } = R.withNormalisation n (applyReductionOptions x r)
 
applyReconstruction : TC A → TC A
applyReconstruction x r@record { reconstruction = false } = x r
applyReconstruction x r@record { reconstruction = true  } = R'.withReconstructed true (x r)
 
applyNoConstraints : TC A → TC A
applyNoConstraints x r@record { noConstraints = false } = x r
applyNoConstraints x r@record { noConstraints = true  } = R'.noConstraints (x r)
 
applyExtContext : Telescope → R.TC A → R.TC A
applyExtContext [] x       = x
applyExtContext (t ∷ ts) x = applyExtContext ts $ (uncurry R.extendContext) t x
 
private
  liftTC : R.TC A → TC A
  liftTC x = λ r → applyExtContext (r .TCEnv.localContext) x
 
  liftTC1 : (A → R.TC B) → A → TC B
  liftTC1 f a = liftTC (f a)
 
  liftTC2 : (A → B → R.TC C) → A → B → TC C
  liftTC2 f a b = liftTC (f a b)
 
  liftTC3 : (A → B → C → R.TC D) → A → B → C → TC D
  liftTC3 f a b c = liftTC (f a b c)
 
module MonadTCI where
  unify             : Term → Term → TC ⊤
  unify             = applyNoConstraints ∘₂ liftTC2 R.unify
 
  typeError         : List ErrorPart → TC A
  typeError         = liftTC1 R.typeError
 
  inferType         : Term → TC Type
  inferType         = applyReconstruction ∘ applyNormalisation ∘ liftTC1 R.inferType
 
  checkType         : Term → Type → TC Term
  checkType         = (applyReconstruction ∘ applyNormalisation) ∘₂ liftTC2 R.checkType
 
  normalise         : Term → TC Term
  normalise         = applyReductionOptions ∘ applyReconstruction ∘ liftTC1 R.normalise
 
  reduce            : Term → TC Term
  reduce            = applyReductionOptions ∘ applyReconstruction ∘ liftTC1 R.reduce
 
  quoteTC           : A → TC Term
  quoteTC           = applyNormalisation ∘ liftTC1 R.quoteTC
 
  unquoteTC         : Term → TC A
  unquoteTC         = liftTC1 R.unquoteTC
 
  quoteωTC          : ∀ {A : Setω} → A → TC Term
  quoteωTC          = λ a → liftTC (R'.quoteωTC a)
 
  freshName         : String → TC Name
  freshName         = liftTC1 R.freshName
 
  declareDef        : Arg Name → Type → TC ⊤
  declareDef        = liftTC2 R.declareDef
 
  declarePostulate  : Arg Name → Type → TC ⊤
  declarePostulate  = liftTC2 R.declarePostulate
 
  defineFun         : Name → List Clause → TC ⊤
  defineFun         = liftTC2 R.defineFun
 
  getType           : Name → TC Type
  getType           = applyReconstruction ∘ liftTC1 R.getType
 
  getDefinition     : Name → TC Definition
  getDefinition     = applyReconstruction ∘ liftTC1 R.getDefinition
 
  blockOnMeta       : Meta → TC A
  blockOnMeta       = liftTC1 R.blockOnMeta
 
  commitTC          : TC ⊤
  commitTC          = liftTC R.commitTC
 
  isMacro           : Name → TC Bool
  isMacro           = liftTC1 R.isMacro
 
  debugPrint        : String → ℕ → List ErrorPart → TC ⊤
  debugPrint        = liftTC3 R.debugPrint
 
  runSpeculative    : TC (A × Bool) → TC A
  runSpeculative    = R.runSpeculative ∘_
 
  getInstances      : Meta → TC (List Term)
  getInstances      = liftTC1 R'.getInstances
 
MonadTC-TCI : MonadTC TC ⦃ Monad-TC ⦄ ⦃ MonadError-TC ⦄
MonadTC-TCI = record { MonadTCI }