module Agda.Interaction.Command.EvalTerm where

import Agda.Interaction.Command.Internal.Parser 

import Agda.Interaction.Base (ComputeMode (..))
import Agda.Interaction.BasicOps hiding (parseExpr)
import Agda.TypeChecking.Monad.Base (TCM)
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.Utils.Pretty (prettyShow)
import Proof.Assistant.Helpers (toBS)

import Data.ByteString (ByteString)

import qualified Data.ByteString.Char8 as BS8

evalTerm :: ByteString -> TCM ByteString
evalTerm :: ByteString -> TCM ByteString
evalTerm ByteString
s = do
  Expr
e <- String -> TCM Expr
parseExpr (ByteString -> String
BS8.unpack ByteString
s)
  Expr
v <- ComputeMode -> Expr -> TCM Expr
evalInCurrent ComputeMode
DefaultCompute Expr
e
  Doc
r <- Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
v
  ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString)
-> (String -> ByteString) -> String -> TCM ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
toBS (String -> TCM ByteString) -> String -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
prettyShow Doc
r