{-# LANGUAGE OverloadedStrings #-}
module Agda.Interaction.Command.EvalIn where

import Agda.Interaction.Base (ComputeMode (..))
import Agda.Interaction.BasicOps (evalInCurrent)
import Agda.Syntax.Abstract.Pretty (prettyA)
import Agda.TypeChecking.Monad.Base (TCM)
import Agda.Utils.Pretty (prettyShow)
import Data.ByteString (ByteString)

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

evalIn :: [ByteString] -> TCM ByteString
evalIn :: [ByteString] -> TCM ByteString
evalIn [ByteString]
s | [ByteString] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ByteString]
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2 =
    do  Doc
d <- [ByteString] -> (InteractionId -> Expr -> TCM Doc) -> TCM Doc
forall a. [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [ByteString]
s ((InteractionId -> Expr -> TCM Doc) -> TCM Doc)
-> (InteractionId -> Expr -> TCM Doc) -> TCM Doc
forall a b. (a -> b) -> a -> b
$ \InteractionId
_ Expr
e -> Expr -> TCM Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (Expr -> TCM Doc) -> TCMT IO Expr -> TCM Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ComputeMode -> Expr -> TCMT IO Expr
evalInCurrent ComputeMode
DefaultCompute Expr
e
        ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString)
-> (Doc -> ByteString) -> Doc -> TCM ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ByteString
toBS (String -> ByteString) -> (Doc -> String) -> Doc -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Pretty a => a -> String
prettyShow (Doc -> TCM ByteString) -> Doc -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ Doc
d
evalIn [ByteString]
_ = ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
":eval metaid expr"