{-# OPTIONS --safe --without-K #-}
--------------------------------------------------------------------------------
-- Types & functions for interacting with tactics/metaprograms
--------------------------------------------------------------------------------

module Reflection.Tactic where

import Reflection as R
open import Class.Monad hiding (Monad-TC)
open import Class.MonadTC
open import Meta.Prelude
open import Meta.Init

open MonadTC ⦃...⦄

private variable
  a : Level
  A : Set a

Tactic = Term → R.TC ⊤
UnquoteDecl = R.TC ⊤

ITactic : Set
ITactic = TC ⊤

initTacEnv : (TCEnv → TCEnv) → ITactic → Tactic
initTacEnv f tac goal = (initTCEnvWithGoal goal) R.>>= tac ∘ f

initTacOpts : ITactic → TCOptions → Tactic
initTacOpts tac opts = initTacEnv (λ env → record env { options = opts }) tac

module _ ⦃ opts : TCOptions ⦄ where

  initTac : ITactic → Tactic
  initTac tac = initTacOpts tac opts

  initUnquoteWithGoal : Term → TC ⊤ → UnquoteDecl
  initUnquoteWithGoal g unq = (initTCEnvWithGoal g) R.>>= unq
                            ∘ (λ env → record env { options = opts })

  initUnquote : TC ⊤ → UnquoteDecl
  initUnquote unq = initUnquoteWithGoal unknown unq

  macro
    byTC : TC A → Tactic
    byTC comp = initTac ((comp >>= quoteTC) >>= unifyWithGoal)

    by : ITactic → Tactic
    by = initTac