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

import Agda.Interaction.Command.Internal.Parser
import Agda.Syntax.Common (InteractionId (..), argNameToString)
import Agda.TypeChecking.Monad.Base (TCM, getMetaInfo)
import Agda.TypeChecking.Monad.Context (getContextTelescope)
import Agda.TypeChecking.Monad.MetaVars (lookupInteractionId, lookupMeta, withMetaInfo)
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.TypeChecking.Reduce (normalise)
import Agda.TypeChecking.Substitute.Class (raise)
import Agda.Utils.Pretty ((<+>), render, text)
import Control.Monad.Except (zipWithM)
import Data.ByteString (ByteString)

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

showContext :: [ByteString] -> TCM ByteString
showContext :: [ByteString] -> TCM ByteString
showContext (ByteString
meta:[ByteString]
args) = 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
meta)
    MetaVariable
mi <- MetaId -> TCMT IO MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta (MetaId -> TCMT IO MetaVariable)
-> TCMT IO MetaId -> TCMT IO MetaVariable
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< InteractionId -> TCMT IO MetaId
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m, MonadTCEnv m) =>
InteractionId -> m MetaId
lookupInteractionId InteractionId
i
    [ByteString] -> ByteString
BS8.unlines ([ByteString] -> ByteString)
-> TCMT IO [ByteString] -> TCM ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Closure Range -> TCMT IO [ByteString] -> TCMT IO [ByteString]
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mi) TCMT IO [ByteString]
displayMore
  where
    display :: (String, a) -> Nat -> m ByteString
display (String
x, a
t) Nat
n = do
      a
t0 <- case [ByteString]
args of
             [ByteString
"normal"] -> a -> m a
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Nat -> a -> a
forall a. Subst a => Nat -> a -> a
raise Nat
n a
t
             [ByteString]
_          -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ Nat -> a -> a
forall a. Subst a => Nat -> a -> a
raise Nat
n a
t
      Doc
d <- a -> m Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
t0
      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
BS8.pack (String -> ByteString) -> String -> ByteString
forall a b. (a -> b) -> a -> b
$ Doc -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ String -> Doc
text (String -> String
argNameToString String
x) Doc -> Doc -> Doc
<+> Doc
":" Doc -> Doc -> Doc
<+> Doc
d
    displayMore :: TCMT IO [ByteString]
displayMore = do
      [(String, Type)]
ctx <- (Dom' Term (String, Type) -> (String, Type))
-> [Dom' Term (String, Type)] -> [(String, Type)]
forall a b. (a -> b) -> [a] -> [b]
List.map Dom' Term (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
I.unDom ([Dom' Term (String, Type)] -> [(String, Type)])
-> (Tele (Dom Type) -> [Dom' Term (String, Type)])
-> Tele (Dom Type)
-> [(String, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> [Dom' Term (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
I.telToList (Tele (Dom Type) -> [(String, Type)])
-> TCMT IO (Tele (Dom Type)) -> TCMT IO [(String, Type)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Applicative m, MonadTCEnv m) =>
m (Tele (Dom Type))
getContextTelescope
      ((String, Type) -> Nat -> TCM ByteString)
-> [(String, Type)] -> [Nat] -> TCMT IO [ByteString]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (String, Type) -> Nat -> TCM ByteString
forall (m :: * -> *) a.
(Normalise a, Subst a, PrettyTCM a, PureTCM m,
 MonadInteractionPoints m, MonadFresh NameId m,
 MonadStConcreteNames m, IsString (m Doc), Null (m Doc),
 Semigroup (m Doc)) =>
(String, a) -> Nat -> m ByteString
display [(String, Type)]
ctx ([Nat] -> TCMT IO [ByteString]) -> [Nat] -> TCMT IO [ByteString]
forall a b. (a -> b) -> a -> b
$ [Nat] -> [Nat]
forall a. [a] -> [a]
reverse ([Nat] -> [Nat]) -> [Nat] -> [Nat]
forall a b. (a -> b) -> a -> b
$ (Nat -> (String, Type) -> Nat)
-> [Nat] -> [(String, Type)] -> [Nat]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> (String, Type) -> Nat
forall a b. a -> b -> a
const [Nat
1..] [(String, Type)]
ctx
showContext [ByteString]
_ = ByteString -> TCM ByteString
forall (f :: * -> *) a. Applicative f => a -> f a
pure ByteString
"context meta"