quox/tests/TypingImpls.idr

36 lines
790 B
Idris

module TypingImpls
import TAP
import public Quox.Typing
import public Quox.Pretty
import public TermImpls
import Derive.Prelude
%language ElabReflection
%runElab derive "Reduce.WhnfError" [Show]
export %hint
showTyContext : (IsQty q, PrettyHL q, Show q) => Show (TyContext q d n)
showTyContext = deriveShow
export %hint
showEqContext : (IsQty q, PrettyHL q, Show q) => Show (EqContext q n)
showEqContext = deriveShow
export %hint
showTypingError : (IsQty q, PrettyHL q, Show q) => Show (Error q)
showTypingError = deriveShow
export
ToInfo WhnfError where
toInfo (MissingEnumArm t ts) =
[("type", "MissingEnumArm"),
("tag", show t),
("list", show ts)]
export
(IsQty q, PrettyHL q) => ToInfo (Error q) where
toInfo err = [("err", show $ prettyError True True err)]