module Agda.Interaction.Command.TypeOf where

import Agda.Interaction.Base (Rewrite (..))
import Agda.Interaction.BasicOps (typeInCurrent)
import Agda.TypeChecking.Monad.Base (TCM)
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.Utils.Pretty (prettyShow)
import Data.ByteString (ByteString)

import Agda.Interaction.Command.Internal.Parser
import Proof.Assistant.Helpers (toBS)

import qualified Data.ByteString.Char8 as BS8

typeOf :: [ByteString] -> TCM ByteString
typeOf :: [ByteString] -> TCM ByteString
typeOf [ByteString]
s =
    do  Expr
e  <- String -> TCM Expr
parseExpr (ByteString -> String
BS8.unpack (ByteString -> String) -> ByteString -> String
forall a b. (a -> b) -> a -> b
$ [ByteString] -> ByteString
BS8.unwords [ByteString]
s)
        Expr
_e0 <- Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
Normalised Expr
e
        Expr
e1 <- Rewrite -> Expr -> TCM Expr
typeInCurrent Rewrite
AsIs Expr
e
        Doc
r <- Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
e1
        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