------------------------------------------------------------------------
-- The Agda standard library
--
-- The TC (Type Checking) monad
------------------------------------------------------------------------
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Reflection.TCM where
 
import Agda.Builtin.Reflection as Builtin
 
open import Reflection.AST.Term
import Reflection.TCM.Format as Format
 
------------------------------------------------------------------------
-- Type errors
 
open Builtin public
  using (ErrorPart; strErr; termErr; nameErr)
 
------------------------------------------------------------------------
-- The monad
 
open Builtin public
  using
  ( TC; bindTC; unify; typeError; inferType; checkType
  ; normalise; reduce
  ; catchTC; quoteTC; unquoteTC
  ; getContext; extendContext; inContext; freshName
  ; declareDef; declarePostulate; defineFun; getType; getDefinition
  ; blockOnMeta; commitTC; isMacro; withNormalisation
  ; debugPrint; noConstraints; runSpeculative
  ; Blocker; blockerMeta; blockerAny; blockerAll; blockTC
  )
  renaming (returnTC to pure)
 
open Format public
  using (typeErrorFmt; debugPrintFmt; errorPartFmt)
 
------------------------------------------------------------------------
-- Utility functions
 
newMeta : Type → TC Term
newMeta = checkType unknown