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

import Agda.Interaction.Base (Rewrite (..))
import Agda.Interaction.BasicOps (typeInMeta)
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)

typeIn :: [ByteString] -> TCM ByteString
typeIn :: [ByteString] -> TCM ByteString
typeIn s :: [ByteString]
s@(ByteString
_:ByteString
_:[ByteString]
_) =
    [ByteString]
-> (InteractionId -> Expr -> TCM ByteString) -> TCM ByteString
forall a. [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [ByteString]
s ((InteractionId -> Expr -> TCM ByteString) -> TCM ByteString)
-> (InteractionId -> Expr -> TCM ByteString) -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ \InteractionId
i Expr
e ->
    do  Expr
e1 <- InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
i Rewrite
Normalised Expr
e
        Expr
_e2 <- InteractionId -> Rewrite -> Expr -> TCM Expr
typeInMeta InteractionId
i 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

typeIn [ByteString]
_ = ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
":typeIn meta expr"