quox/tests/TypingImpls.idr

module TypingImpls

import TAP
import public Quox.Typing
import public Quox.Pretty
import Quox.Equal
import Quox.Typechecker
import Control.Monad.ST.Extra
import PrettyExtra

import Derive.Prelude
%language ElabReflection


export
ToInfo Error where
  toInfo err =
    let str = render (Opts 60) $ runPrettyDef $ prettyError True err in
    [("err", str)]


export
runEqual : Definitions -> Eff Equal a -> Either Error a
runEqual defs act = runSTErr $ do
  runEff act $ with Union.(::)
    [handleExcept (\e => stLeft e),
     handleReaderConst defs,
     handleStateSTRef !(newSTRef' 0),
     handleLogDiscardST !(newSTRef' 0)]

export
runTC : Definitions -> Eff TC a -> Either Error a
runTC = runEqual