module Agda.Interaction.Command.RefineMeta where

import Agda.TypeChecking.Monad.Base (TCM)
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.Utils.Pretty (prettyShow)
import Data.ByteString (ByteString)

import Agda.Interaction.Base (UseForce (..))
import Agda.Interaction.BasicOps (refine)
import Agda.Interaction.Command.Internal.Parser
import Proof.Assistant.Helpers (toBS)

refineMeta :: [ByteString] -> TCM ByteString
refineMeta :: [ByteString] -> TCM ByteString
refineMeta [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
  Expr
expr <- [ByteString] -> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a. [ByteString] -> (InteractionId -> Expr -> TCM a) -> TCM a
actOnMeta [ByteString]
s ((InteractionId -> Expr -> TCM Expr) -> TCM Expr)
-> (InteractionId -> Expr -> TCM Expr) -> TCM Expr
forall a b. (a -> b) -> a -> b
$ \ InteractionId
ii Expr
e -> UseForce -> InteractionId -> Maybe Range -> Expr -> TCM Expr
refine UseForce
WithoutForce InteractionId
ii Maybe Range
forall a. Maybe a
Nothing Expr
e
  Doc
r <- Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Expr
expr
  ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString) -> ByteString -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ String -> ByteString
toBS (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ Doc -> String
forall a. Pretty a => a -> String
prettyShow Doc
r
refineMeta [ByteString]
_ = ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> TCM ByteString) -> ByteString -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ String -> ByteString
toBS (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ String
": refine" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" metaid expr"