{-# OPTIONS --without-K --safe #-}

open import Prelude

module Utils.Error where

open import Utils.Reflection.Core
open import Utils.Reflection.Show

private variable
  A : Set _

notEndIn : ErrorPart → ErrorPart → TC A
notEndIn s n = typeError (strErr "Type of"
                       ∷ s
                       ∷ strErr "does not end in "
                       ∷ n
                       ∷ [])

#idxNotMatch : TC A
#idxNotMatch = typeError [ strErr "number of indices doesn't match." ]

notλ : Term → TC A
notλ t = typeError $ strErr (show t) ∷ strErr " cannot be reduced further to a λ-abstraction" ∷ []

notDef : Term → TC A
notDef t = typeError $ termErr t ∷ strErr " is not a definition." ∷ []

notApp : Term → TC A
notApp t = typeError $ termErr t ∷ strErr " is not an application witha name." ∷ []

notFun : Name → TC A
notFun d = typeError $ nameErr d ∷ [ strErr " is not a function." ]

notData : Term → TC A
notData t = typeError $ termErr t ∷ [ strErr " is not a datatype." ]

IMPOSSIBLE : TC A
IMPOSSIBLE = typeError $ [ strErr "An impossible event occurs." ]

IMPOSSIBLE-term : Term → TC A
IMPOSSIBLE-term t = typeError $ termErr t ∷ [ strErr " should not occur" ]