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

import Agda.Interaction.Base (OutputConstraint (..),  OutputForm (..), Rewrite (..))
import Agda.Interaction.BasicOps
  (outputFormId, typeOfMeta, typesOfHiddenMetas, typesOfVisibleMetas)
import Agda.Syntax.Abstract.Pretty (prettyA)
import Agda.Syntax.Common (InteractionId (..))
import Agda.Syntax.Position (noRange)
import Agda.TypeChecking.Monad.Base (TCM, nmid)
import Agda.TypeChecking.Monad.MetaVars
  (getInteractionRange, getMetaRange, withInteractionId, withMetaId)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Pretty (prettyShow, render)
import Data.ByteString (ByteString)

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

import qualified Agda.Syntax.Internal as I
import qualified Data.ByteString.Char8 as BS8

showMetas :: [ByteString] -> TCM ByteString
showMetas :: [ByteString] -> TCM ByteString
showMetas [ByteString
m] =
    do  InteractionId
i <- Nat -> InteractionId
InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Nat
forall a. Read a => String -> TCM a
readM (ByteString -> String
BS8.unpack ByteString
m)
        InteractionId -> TCM ByteString -> TCM ByteString
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i (TCM ByteString -> TCM ByteString)
-> TCM ByteString -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ do
          OutputConstraint Expr InteractionId
s <- Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta Rewrite
AsIs InteractionId
i
          Range
r <- InteractionId -> TCMT IO Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
          Doc
d <- OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint Expr InteractionId
s
          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
render Doc
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Pretty a => a -> String
prettyShow Range
r
showMetas [ByteString
m,ByteString
"normal"] =
    do  InteractionId
i <- Nat -> InteractionId
InteractionId (Nat -> InteractionId) -> TCMT IO Nat -> TCMT IO InteractionId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO Nat
forall a. Read a => String -> TCM a
readM (ByteString -> String
BS8.unpack ByteString
m)
        InteractionId -> TCM ByteString -> TCM ByteString
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
i (TCM ByteString -> TCM ByteString)
-> TCM ByteString -> TCM ByteString
forall a b. (a -> b) -> a -> b
$ do
          Doc
s <- OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA (OutputConstraint Expr InteractionId -> TCMT IO Doc)
-> TCM (OutputConstraint Expr InteractionId) -> TCMT IO Doc
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
typeOfMeta Rewrite
Normalised InteractionId
i
          Range
r <- InteractionId -> TCMT IO Range
forall (m :: * -> *).
(MonadInteractionPoints m, MonadFail m, MonadError TCErr m) =>
InteractionId -> m Range
getInteractionRange InteractionId
i
          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
render Doc
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Pretty a => a -> String
prettyShow Range
r
showMetas [] =
    do  [OutputConstraint Expr InteractionId]
interactionMetas <- Rewrite -> TCM [OutputConstraint Expr InteractionId]
typesOfVisibleMetas Rewrite
AsIs
        [OutputConstraint Expr NamedMeta]
hiddenMetas      <- Rewrite -> TCM [OutputConstraint Expr NamedMeta]
typesOfHiddenMetas  Rewrite
AsIs
        [ByteString]
shownInteractionMetas <- (OutputConstraint Expr InteractionId -> TCM ByteString)
-> [OutputConstraint Expr InteractionId] -> TCMT IO [ByteString]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OutputConstraint Expr InteractionId -> TCM ByteString
forall (m :: * -> *) a.
(MonadError TCErr m, MonadTrace m, ToConcrete a,
 Pretty (ConOfAbs a), MonadStConcreteNames m, HasOptions m,
 HasBuiltins m, MonadDebug m) =>
OutputConstraint a InteractionId -> m ByteString
printII [OutputConstraint Expr InteractionId]
interactionMetas
        [ByteString]
shownHiddenMetas <- (OutputConstraint Expr NamedMeta -> TCM ByteString)
-> [OutputConstraint Expr NamedMeta] -> TCMT IO [ByteString]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM OutputConstraint Expr NamedMeta -> TCM ByteString
forall (m :: * -> *) a.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
 MonadStConcreteNames m, HasOptions m, HasBuiltins m,
 MonadDebug m) =>
OutputConstraint a NamedMeta -> m ByteString
printM [OutputConstraint Expr NamedMeta]
hiddenMetas
        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
$ [ByteString] -> ByteString
BS8.unlines
          [ ByteString
"Interaction metas: " ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> [ByteString] -> ByteString
BS8.unwords [ByteString]
shownInteractionMetas
          , ByteString
""
          , ByteString
"Hidden metas: " ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> [ByteString] -> ByteString
BS8.unwords [ByteString]
shownHiddenMetas
          ]
    where
        showII :: OutputConstraint a InteractionId -> m Doc
showII OutputConstraint a InteractionId
o = InteractionId -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m,
 MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId (OutputForm a InteractionId -> InteractionId
forall a b. OutputForm a b -> b
outputFormId (OutputForm a InteractionId -> InteractionId)
-> OutputForm a InteractionId -> InteractionId
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint a InteractionId
-> OutputForm a InteractionId
forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
I.alwaysUnblock OutputConstraint a InteractionId
o) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint a InteractionId -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint a InteractionId
o
        showM :: OutputConstraint a NamedMeta -> m Doc
showM  OutputConstraint a NamedMeta
o = MetaId -> m Doc -> m Doc
forall (m :: * -> *) a.
(MonadFail m, MonadTCEnv m, ReadTCState m, MonadTrace m) =>
MetaId -> m a -> m a
withMetaId (NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputForm a NamedMeta -> NamedMeta
forall a b. OutputForm a b -> b
outputFormId (OutputForm a NamedMeta -> NamedMeta)
-> OutputForm a NamedMeta -> NamedMeta
forall a b. (a -> b) -> a -> b
$ Range
-> [ProblemId]
-> Blocker
-> OutputConstraint a NamedMeta
-> OutputForm a NamedMeta
forall a b.
Range
-> [ProblemId] -> Blocker -> OutputConstraint a b -> OutputForm a b
OutputForm Range
forall a. Range' a
noRange [] Blocker
I.alwaysUnblock OutputConstraint a NamedMeta
o) (m Doc -> m Doc) -> m Doc -> m Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint a NamedMeta -> m Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyA OutputConstraint a NamedMeta
o

        metaId :: OutputConstraint a p -> p
metaId (OfType p
i a
_) = p
i
        metaId (JustType p
i) = p
i
        metaId (JustSort p
i) = p
i
        metaId (Assign p
i a
_e) = p
i
        metaId OutputConstraint a p
_ = p
forall a. HasCallStack => a
__IMPOSSIBLE__
        printM :: OutputConstraint a NamedMeta -> m ByteString
printM OutputConstraint a NamedMeta
x = do
            Range
r <- MetaId -> m Range
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m Range
getMetaRange (MetaId -> m Range) -> MetaId -> m Range
forall a b. (a -> b) -> a -> b
$ NamedMeta -> MetaId
nmid (NamedMeta -> MetaId) -> NamedMeta -> MetaId
forall a b. (a -> b) -> a -> b
$ OutputConstraint a NamedMeta -> NamedMeta
forall a p. OutputConstraint a p -> p
metaId OutputConstraint a NamedMeta
x
            Doc
d <- OutputConstraint a NamedMeta -> m Doc
forall (m :: * -> *) a.
(MonadTrace m, ToConcrete a, Pretty (ConOfAbs a),
 MonadStConcreteNames m, HasOptions m, HasBuiltins m,
 MonadDebug m) =>
OutputConstraint a NamedMeta -> m Doc
showM OutputConstraint a NamedMeta
x
            ByteString -> m ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> m ByteString) -> ByteString -> m ByteString
forall a b. (a -> b) -> a -> b
$ String -> ByteString
toBS (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ Doc -> String
render Doc
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"  [ at " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Range -> String
forall a. Pretty a => a -> String
prettyShow Range
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ]"
        printII :: OutputConstraint a InteractionId -> m ByteString
printII OutputConstraint a InteractionId
x = do
          Doc
d <- OutputConstraint a InteractionId -> m Doc
forall (m :: * -> *) a.
(MonadError TCErr m, MonadTrace m, ToConcrete a,
 Pretty (ConOfAbs a), MonadStConcreteNames m, HasOptions m,
 HasBuiltins m, MonadDebug m) =>
OutputConstraint a InteractionId -> m Doc
showII OutputConstraint a InteractionId
x
          ByteString -> m ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ByteString -> m ByteString) -> ByteString -> m ByteString
forall a b. (a -> b) -> a -> b
$ String -> ByteString
toBS (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ Doc -> String
render Doc
d
showMetas [ByteString]
_ = ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
":meta [metaid]"