module Agda.Interaction.EmacsTop
( mimicGHCi
, namedMetaOf
, showGoals
, showInfoError
, explainWhyInScope
, prettyTypeOfMeta
) where
import Control.Monad.State hiding (state)
import qualified Data.List as List
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.Syntax.Abstract.Pretty (prettyATop)
import Agda.Syntax.Abstract as A
import Agda.Syntax.Concrete as C
import Agda.TypeChecking.Errors (prettyError)
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings, prettyTCWarnings')
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..))
import Agda.Interaction.AgdaTop
import Agda.Interaction.Base
import Agda.Interaction.BasicOps as B
import Agda.Interaction.Response as R
import Agda.Interaction.EmacsCommand hiding (putResponse)
import Agda.Interaction.Highlighting.Emacs
import Agda.Interaction.Highlighting.Precise (TokenBased(..))
import Agda.Interaction.InteractionTop (localStateCommandM)
import Agda.Interaction.Imports (getAllWarningsOfTCErr)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Null (empty)
import Agda.Utils.Maybe
import Agda.Utils.Pretty
import Agda.Utils.String
import Agda.Utils.Time (CPUTime)
import Agda.VersionCommit
mimicGHCi :: TCM () -> TCM ()
mimicGHCi :: TCM () -> TCM ()
mimicGHCi = InteractionOutputCallback -> String -> TCM () -> TCM ()
repl (IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ())
-> ([Lisp String] -> IO ()) -> [Lisp String] -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lisp String -> IO ()) -> [Lisp String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Lisp String -> IO ()
forall a. Show a => a -> IO ()
print ([Lisp String] -> TCM ())
-> (Response -> TCMT IO [Lisp String]) -> InteractionOutputCallback
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> TCMT IO [Lisp String]
lispifyResponse) "Agda2> "
lispifyResponse :: Response -> TCM [Lisp String]
lispifyResponse :: Response -> TCMT IO [Lisp String]
lispifyResponse (Resp_HighlightingInfo info :: HighlightingInfo
info remove :: RemoveTokenBasedHighlighting
remove method :: HighlightingMethod
method modFile :: ModuleToSource
modFile) =
(Lisp String -> [Lisp String] -> [Lisp String]
forall a. a -> [a] -> [a]
:[]) (Lisp String -> [Lisp String])
-> TCMT IO (Lisp String) -> TCMT IO [Lisp String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Lisp String) -> TCMT IO (Lisp String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO (Lisp String)
lispifyHighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile)
lispifyResponse (Resp_DisplayInfo info :: DisplayInfo
info) = DisplayInfo -> TCMT IO [Lisp String]
lispifyDisplayInfo DisplayInfo
info
lispifyResponse (Resp_ClearHighlighting tokenBased :: TokenBased
tokenBased) =
[Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> Lisp String
forall a. a -> Lisp a
A "agda2-highlight-clear" Lisp String -> [Lisp String] -> [Lisp String]
forall a. a -> [a] -> [a]
:
case TokenBased
tokenBased of
NotOnlyTokenBased -> []
TokenBased ->
[ Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (TokenBased -> Lisp String
lispifyTokenBased TokenBased
tokenBased) ]
]
lispifyResponse Resp_DoneAborting = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A "agda2-abort-done" ] ]
lispifyResponse Resp_DoneExiting = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A "agda2-exit-done" ] ]
lispifyResponse Resp_ClearRunningInfo = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Lisp String
clearRunningInfo ]
lispifyResponse (Resp_RunningInfo n :: Int
n s :: String
s)
| Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 1 = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ String -> Lisp String
displayRunningInfo String
s ]
| Bool
otherwise = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [String -> Lisp String
forall a. a -> Lisp a
A "agda2-verbose", String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote String
s)] ]
lispifyResponse (Resp_Status s :: Status
s)
= [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A "agda2-status-action"
, String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate "," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes [Maybe String
checked, Maybe String
showImpl])
]
]
where
checked :: Maybe String
checked = Bool -> String -> Maybe String
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sChecked Status
s) "Checked"
showImpl :: Maybe String
showImpl = Bool -> String -> Maybe String
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sShowImplicitArguments Status
s) "ShowImplicit"
lispifyResponse (Resp_JumpToError f :: String
f p :: Int32
p) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp String -> Lisp String
lastTag 3 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$
[Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A "agda2-maybe-goto", Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [String -> Lisp String
forall a. a -> Lisp a
A (String -> String
quote String
f), String -> Lisp String
forall a. a -> Lisp a
A ".", String -> Lisp String
forall a. a -> Lisp a
A (Int32 -> String
forall a. Show a => a -> String
show Int32
p)] ]
]
lispifyResponse (Resp_InteractionPoints is :: [InteractionId]
is) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp String -> Lisp String
lastTag 1 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$
[Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [String -> Lisp String
forall a. a -> Lisp a
A "agda2-goals-action", Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ (InteractionId -> Lisp String) -> [InteractionId] -> [Lisp String]
forall a b. (a -> b) -> [a] -> [b]
map InteractionId -> Lisp String
showNumIId [InteractionId]
is]
]
lispifyResponse (Resp_GiveAction ii :: InteractionId
ii s :: GiveResult
s)
= [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A "agda2-give-action", InteractionId -> Lisp String
showNumIId InteractionId
ii, String -> Lisp String
forall a. a -> Lisp a
A String
s' ] ]
where
s' :: String
s' = case GiveResult
s of
Give_String str :: String
str -> String -> String
quote String
str
Give_Paren -> "'paren"
Give_NoParen -> "'no-paren"
lispifyResponse (Resp_MakeCase ii :: InteractionId
ii variant :: MakeCaseVariant
variant pcs :: [String]
pcs) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp String -> Lisp String
lastTag 2 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A String
cmd, Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ (String -> Lisp String) -> [String] -> [Lisp String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String)
-> (String -> String) -> String -> Lisp String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
quote) [String]
pcs ] ]
where
cmd :: String
cmd = case MakeCaseVariant
variant of
R.Function -> "agda2-make-case-action"
R.ExtendedLambda -> "agda2-make-case-action-extendlam"
lispifyResponse (Resp_SolveAll ps :: [(InteractionId, Expr)]
ps) = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp String -> Lisp String
lastTag 2 (Lisp String -> Lisp String) -> Lisp String -> Lisp String
forall a b. (a -> b) -> a -> b
$
[Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A "agda2-solveAll-action", Lisp String -> Lisp String
forall a. Lisp a -> Lisp a
Q (Lisp String -> Lisp String)
-> ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L ([Lisp String] -> Lisp String) -> [Lisp String] -> Lisp String
forall a b. (a -> b) -> a -> b
$ ((InteractionId, Expr) -> [Lisp String])
-> [(InteractionId, Expr)] -> [Lisp String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (InteractionId, Expr) -> [Lisp String]
forall a. Pretty a => (InteractionId, a) -> [Lisp String]
prn [(InteractionId, Expr)]
ps ]
]
where
prn :: (InteractionId, a) -> [Lisp String]
prn (ii :: InteractionId
ii,e :: a
e)= [InteractionId -> Lisp String
showNumIId InteractionId
ii, String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> String
quote (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Pretty a => a -> String
prettyShow a
e]
lispifyDisplayInfo :: DisplayInfo -> TCM [Lisp String]
lispifyDisplayInfo :: DisplayInfo -> TCMT IO [Lisp String]
lispifyDisplayInfo info :: DisplayInfo
info = case DisplayInfo
info of
Info_CompilationOk ws :: WarningsAndNonFatalErrors
ws -> do
String
warnings <- [TCWarning] -> TCM String
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
ws)
String
errors <- [TCWarning] -> TCM String
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
ws)
let (body :: String
body, _) = String -> String -> String -> (String, String)
formatWarningsAndErrors
"The module was successfully compiled.\n"
String
warnings
String
errors
String -> String -> TCMT IO [Lisp String]
format String
body "*Compilation result*"
Info_Constraints s :: [OutputForm Expr Expr]
s -> String -> String -> TCMT IO [Lisp String]
format (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (OutputForm Expr Expr -> Doc) -> [OutputForm Expr Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm Expr Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [OutputForm Expr Expr]
s) "*Constraints*"
Info_AllGoalsWarnings ms :: Goals
ms ws :: WarningsAndNonFatalErrors
ws -> do
String
goals <- Goals -> TCM String
showGoals Goals
ms
String
warnings <- [TCWarning] -> TCM String
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
ws)
String
errors <- [TCWarning] -> TCM String
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
ws)
let (body :: String
body, title :: String
title) = String -> String -> String -> (String, String)
formatWarningsAndErrors String
goals String
warnings String
errors
String -> String -> TCMT IO [Lisp String]
format String
body ("*All" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
title String -> String -> String
forall a. [a] -> [a] -> [a]
++ "*")
Info_Auto s :: String
s -> String -> String -> TCMT IO [Lisp String]
format String
s "*Auto*"
Info_Error err :: Info_Error
err -> do
String
s <- Info_Error -> TCM String
showInfoError Info_Error
err
String -> String -> TCMT IO [Lisp String]
format String
s "*Error*"
Info_Time s :: CPUTime
s -> String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ CPUTime -> Doc
prettyTimed CPUTime
s) "*Time*"
Info_NormalForm state :: CommandState
state cmode :: ComputeMode
cmode time :: Maybe CPUTime
time expr :: Expr
expr -> do
Doc
exprDoc <- StateT CommandState TCM Doc -> CommandState -> TCM Doc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState TCM Doc
prettyExpr CommandState
state
let doc :: Doc
doc = Doc -> (CPUTime -> Doc) -> Maybe CPUTime -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty CPUTime -> Doc
prettyTimed Maybe CPUTime
time Doc -> Doc -> Doc
$$ Doc
exprDoc
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Normal Form*"
where
prettyExpr :: StateT CommandState TCM Doc
prettyExpr = StateT CommandState TCM Doc -> StateT CommandState TCM Doc
forall a. CommandM a -> CommandM a
localStateCommandM
(StateT CommandState TCM Doc -> StateT CommandState TCM Doc)
-> StateT CommandState TCM Doc -> StateT CommandState TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> StateT CommandState TCM Doc
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
(TCM Doc -> StateT CommandState TCM Doc)
-> TCM Doc -> StateT CommandState TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall a. TCM a -> TCM a
B.atTopLevel
(TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
(TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (if ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
cmode then TCM Doc -> TCM Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCM Doc -> TCM Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
(TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ (ComputeMode -> Expr -> TCM Doc
B.showComputed ComputeMode
cmode)
(Expr -> TCM Doc) -> Expr -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Expr
expr
Info_InferredType state :: CommandState
state time :: Maybe CPUTime
time expr :: Expr
expr -> do
Doc
exprDoc <- StateT CommandState TCM Doc -> CommandState -> TCM Doc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState TCM Doc
prettyExpr CommandState
state
let doc :: Doc
doc = Doc -> (CPUTime -> Doc) -> Maybe CPUTime -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty CPUTime -> Doc
prettyTimed Maybe CPUTime
time Doc -> Doc -> Doc
$$ Doc
exprDoc
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Inferred Type*"
where
prettyExpr :: StateT CommandState TCM Doc
prettyExpr = StateT CommandState TCM Doc -> StateT CommandState TCM Doc
forall a. CommandM a -> CommandM a
localStateCommandM
(StateT CommandState TCM Doc -> StateT CommandState TCM Doc)
-> StateT CommandState TCM Doc -> StateT CommandState TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> StateT CommandState TCM Doc
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
(TCM Doc -> StateT CommandState TCM Doc)
-> TCM Doc -> StateT CommandState TCM Doc
forall a b. (a -> b) -> a -> b
$ TCM Doc -> TCM Doc
forall a. TCM a -> TCM a
B.atTopLevel
(TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
TCP.prettyA
(Expr -> TCM Doc) -> Expr -> TCM Doc
forall a b. (a -> b) -> a -> b
$ Expr
expr
Info_ModuleContents modules :: [Name]
modules tel :: Telescope
tel types :: [(Name, Type)]
types -> do
Doc
doc <- TCM Doc -> TCM Doc
forall a. TCM a -> TCM a
localTCState (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
[(String, Doc)]
typeDocs <- Telescope -> TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext Telescope
tel (TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)])
-> TCMT IO [(String, Doc)] -> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$ [(Name, Type)]
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
types (((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)])
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$ \ (x :: Name
x, t :: Type
t) -> do
Doc
doc <- Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
(String, Doc) -> TCMT IO (String, Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x, ":" Doc -> Doc -> Doc
<+> Doc
doc)
Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
[ "Modules"
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
pretty [Name]
modules
, "Names"
, Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Int -> [(String, Doc)] -> Doc
align 10 [(String, Doc)]
typeDocs
]
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Module contents*"
Info_SearchAbout hits :: [(Name, Type)]
hits names :: String
names -> do
[(String, Doc)]
hitDocs <- [(Name, Type)]
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [(Name, Type)]
hits (((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)])
-> ((Name, Type) -> TCMT IO (String, Doc))
-> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$ \ (x :: Name
x, t :: Type
t) -> do
Doc
doc <- Type -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t
(String, Doc) -> TCMT IO (String, Doc)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x, ":" Doc -> Doc -> Doc
<+> Doc
doc)
let doc :: Doc
doc = "Definitions about" Doc -> Doc -> Doc
<+>
String -> Doc
text (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate ", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String]
words String
names) Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (Int -> [(String, Doc)] -> Doc
align 10 [(String, Doc)]
hitDocs)
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Search About*"
Info_WhyInScope s :: String
s cwd :: String
cwd v :: Maybe LocalVar
v xs :: [AbstractName]
xs ms :: [AbstractModule]
ms -> do
Doc
doc <- String
-> String
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> TCM Doc
explainWhyInScope String
s String
cwd Maybe LocalVar
v [AbstractName]
xs [AbstractModule]
ms
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Scope Info*"
Info_Context ii :: InteractionId
ii ctx :: [ResponseContextEntry]
ctx -> do
Doc
doc <- TCM Doc -> TCM Doc
forall a. TCM a -> TCM a
localTCState (InteractionId -> Bool -> [ResponseContextEntry] -> TCM Doc
prettyResponseContext InteractionId
ii Bool
False [ResponseContextEntry]
ctx)
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Context*"
Info_Intro_NotFound -> String -> String -> TCMT IO [Lisp String]
format "No introduction forms found." "*Intro*"
Info_Intro_ConstructorUnknown ss :: [String]
ss -> do
let doc :: Doc
doc = [Doc] -> Doc
sep [ "Don't know which constructor to introduce of"
, let mkOr :: [String] -> [Doc]
mkOr [] = []
mkOr [x :: String
x, y :: String
y] = [String -> Doc
text String
x Doc -> Doc -> Doc
<+> "or" Doc -> Doc -> Doc
<+> String -> Doc
text String
y]
mkOr (x :: String
x:xs :: [String]
xs) = String -> Doc
text String
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [String] -> [Doc]
mkOr [String]
xs
in Int -> Doc -> Doc
nest 2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([String] -> [Doc]
mkOr [String]
ss)
]
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Intro*"
Info_Version -> String -> String -> TCMT IO [Lisp String]
format ("Agda version " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
versionWithCommitInfo) "*Agda Version*"
Info_GoalSpecific ii :: InteractionId
ii kind :: GoalDisplayInfo
kind -> InteractionId -> GoalDisplayInfo -> TCMT IO [Lisp String]
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo
kind
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String]
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCMT IO [Lisp String]
lispifyGoalSpecificDisplayInfo ii :: InteractionId
ii kind :: GoalDisplayInfo
kind = TCMT IO [Lisp String] -> TCMT IO [Lisp String]
forall a. TCM a -> TCM a
localTCState (TCMT IO [Lisp String] -> TCMT IO [Lisp String])
-> TCMT IO [Lisp String] -> TCMT IO [Lisp String]
forall a b. (a -> b) -> a -> b
$ InteractionId -> TCMT IO [Lisp String] -> TCMT IO [Lisp String]
forall a. InteractionId -> TCM a -> TCM a
B.withInteractionId InteractionId
ii (TCMT IO [Lisp String] -> TCMT IO [Lisp String])
-> TCMT IO [Lisp String] -> TCMT IO [Lisp String]
forall a b. (a -> b) -> a -> b
$
case GoalDisplayInfo
kind of
Goal_HelperFunction helperType :: OutputConstraint' Expr Expr
helperType -> do
Doc
doc <- TCM Doc -> TCM Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint' Expr Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint' Expr Expr
helperType
[Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp String] -> Lisp String
forall a. [Lisp a] -> Lisp a
L [ String -> Lisp String
forall a. a -> Lisp a
A "agda2-info-action-and-copy"
, String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> String
quote "*Helper function*"
, String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ String -> String
quote (Doc -> String
render Doc
doc String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n")
, String -> Lisp String
forall a. a -> Lisp a
A "nil"
]
]
Goal_NormalForm cmode :: ComputeMode
cmode expr :: Expr
expr -> do
Doc
doc <- ComputeMode -> Expr -> TCM Doc
showComputed ComputeMode
cmode Expr
expr
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Normal Form*"
Goal_GoalType norm :: Rewrite
norm aux :: GoalTypeAux
aux ctx :: [ResponseContextEntry]
ctx bndry :: [IPBoundary' Expr]
bndry constraints :: [OutputForm Expr Expr]
constraints -> do
Doc
ctxDoc <- InteractionId -> Bool -> [ResponseContextEntry] -> TCM Doc
prettyResponseContext InteractionId
ii Bool
True [ResponseContextEntry]
ctx
Doc
goalDoc <- Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta Rewrite
norm InteractionId
ii
Doc
auxDoc <- case GoalTypeAux
aux of
GoalOnly -> Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
forall a. Null a => a
empty
GoalAndHave expr :: Expr
expr -> do
Doc
doc <- Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "Have:" Doc -> Doc -> Doc
<+> Doc
doc
GoalAndElaboration term :: Term
term -> do
Doc
doc <- Term -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM Term
term
Doc -> TCM Doc
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCM Doc) -> Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "Elaborates to:" Doc -> Doc -> Doc
<+> Doc
doc
let boundaryDoc :: [Doc]
boundaryDoc
| [IPBoundary' Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IPBoundary' Expr]
bndry = []
| Bool
otherwise = [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter "Boundary"
, [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (IPBoundary' Expr -> Doc) -> [IPBoundary' Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map IPBoundary' Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [IPBoundary' Expr]
bndry
]
let constraintsDoc :: [Doc]
constraintsDoc = if ([OutputForm Expr Expr] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OutputForm Expr Expr]
constraints)
then []
else [ String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter "Constraints"
, [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (OutputForm Expr Expr -> Doc) -> [OutputForm Expr Expr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm Expr Expr -> Doc
forall a. Pretty a => a -> Doc
pretty [OutputForm Expr Expr]
constraints
]
let doc :: Doc
doc = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$
[ "Goal:" Doc -> Doc -> Doc
<+> Doc
goalDoc
, Doc
auxDoc
, [Doc] -> Doc
vcat [Doc]
boundaryDoc
, String -> Doc
text (Int -> Char -> String
forall a. Int -> a -> [a]
replicate 60 '\x2014')
, Doc
ctxDoc
] [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc]
constraintsDoc
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Goal type etc.*"
Goal_CurrentGoal norm :: Rewrite
norm -> do
Doc
doc <- Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta Rewrite
norm InteractionId
ii
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Current Goal*"
Goal_InferredType expr :: Expr
expr -> do
Doc
doc <- Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
String -> String -> TCMT IO [Lisp String]
format (Doc -> String
render Doc
doc) "*Inferred Type*"
format :: String -> String -> TCM [Lisp String]
format :: String -> String -> TCMT IO [Lisp String]
format content :: String
content bufname :: String
bufname = [Lisp String] -> TCMT IO [Lisp String]
forall (m :: * -> *) a. Monad m => a -> m a
return [ Bool -> String -> String -> Lisp String
display_info' Bool
False String
bufname String
content ]
lastTag :: Integer -> Lisp String -> Lisp String
lastTag :: Integer -> Lisp String -> Lisp String
lastTag n :: Integer
n r :: Lisp String
r = Lisp String -> Lisp String -> Lisp String
forall a. Lisp a -> Lisp a -> Lisp a
Cons (Lisp String -> Lisp String -> Lisp String
forall a. Lisp a -> Lisp a -> Lisp a
Cons (String -> Lisp String
forall a. a -> Lisp a
A "last") (String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String) -> String -> Lisp String
forall a b. (a -> b) -> a -> b
$ Integer -> String
forall a. Show a => a -> String
show Integer
n)) Lisp String
r
showNumIId :: InteractionId -> Lisp String
showNumIId :: InteractionId -> Lisp String
showNumIId = String -> Lisp String
forall a. a -> Lisp a
A (String -> Lisp String)
-> (InteractionId -> String) -> InteractionId -> Lisp String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> String)
-> (InteractionId -> Int) -> InteractionId -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId -> Int
interactionId
formatWarningsAndErrors :: String -> String -> String -> (String, String)
formatWarningsAndErrors :: String -> String -> String -> (String, String)
formatWarningsAndErrors g :: String
g w :: String
w e :: String
e = (String
body, String
title)
where
isG :: Bool
isG = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
g
isW :: Bool
isW = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
w
isE :: Bool
isE = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
e
title :: String
title = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate "," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes
[ " Goals" String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
, " Errors" String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
, " Warnings" String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isW
, " Done" String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool
isG Bool -> Bool -> Bool
|| Bool
isW Bool -> Bool -> Bool
|| Bool
isE))
]
body :: String
body = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes
[ String
g String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
, String -> String
delimiter "Errors" String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool
isE Bool -> Bool -> Bool
&& (Bool
isG Bool -> Bool -> Bool
|| Bool
isW))
, String
e String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
, String -> String
delimiter "Warnings" String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool
isW Bool -> Bool -> Bool
&& (Bool
isG Bool -> Bool -> Bool
|| Bool
isE))
, String
w String -> Maybe () -> Maybe String
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isW
]
showInfoError :: Info_Error -> TCM String
showInfoError :: Info_Error -> TCM String
showInfoError (Info_GenericError err :: TCErr
err) = do
String
e <- TCErr -> TCM String
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm String
prettyError TCErr
err
[String]
w <- [TCWarning] -> TCM [String]
prettyTCWarnings' ([TCWarning] -> TCM [String])
-> TCMT IO [TCWarning] -> TCM [String]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err
let errorMsg :: String
errorMsg = if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
w
then String
e
else String -> String
delimiter "Error" String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e
let warningMsg :: String
warningMsg = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> String
delimiter "Warning(s)"
String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [String]
w
String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCM String) -> String -> TCM String
forall a b. (a -> b) -> a -> b
$ if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
w
then String
errorMsg
else String
errorMsg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
warningMsg
showInfoError (Info_CompilationError warnings :: [TCWarning]
warnings) = do
String
s <- [TCWarning] -> TCM String
prettyTCWarnings [TCWarning]
warnings
String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCM String) -> String -> TCM String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ "You need to fix the following errors before you can compile"
, "the module:"
, ""
, String
s
]
showInfoError (Info_HighlightingParseError ii :: InteractionId
ii) =
String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCM String) -> String -> TCM String
forall a b. (a -> b) -> a -> b
$ "Highlighting failed to parse expression in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
showInfoError (Info_HighlightingScopeCheckError ii :: InteractionId
ii) =
String -> TCM String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> TCM String) -> String -> TCM String
forall a b. (a -> b) -> a -> b
$ "Highlighting failed to scope check expression in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ InteractionId -> String
forall a. Show a => a -> String
show InteractionId
ii
explainWhyInScope :: FilePath
-> String
-> (Maybe LocalVar)
-> [AbstractName]
-> [AbstractModule]
-> TCM Doc
explainWhyInScope :: String
-> String
-> Maybe LocalVar
-> [AbstractName]
-> [AbstractModule]
-> TCM Doc
explainWhyInScope s :: String
s _ Nothing [] [] = String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TCP.text (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not in scope.")
explainWhyInScope s :: String
s _ v :: Maybe LocalVar
v xs :: [AbstractName]
xs ms :: [AbstractModule]
ms = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.vcat
[ String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TCP.text (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is in scope as")
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.vcat [Maybe LocalVar -> [AbstractName] -> TCM Doc
variable Maybe LocalVar
v [AbstractName]
xs, [AbstractModule] -> TCM Doc
modules [AbstractModule]
ms]
]
where
variable :: Maybe LocalVar -> [AbstractName] -> TCM Doc
variable Nothing vs :: [AbstractName]
vs = [AbstractName] -> TCM Doc
names [AbstractName]
vs
variable (Just x :: LocalVar
x) vs :: [AbstractName]
vs
| [AbstractName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [AbstractName]
vs = TCM Doc
asVar
| Bool
otherwise = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.vcat
[ [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.sep [ TCM Doc
asVar, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ LocalVar -> TCM Doc
shadowing LocalVar
x]
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ [AbstractName] -> TCM Doc
names [AbstractName]
vs
]
where
asVar :: TCM Doc
asVar :: TCM Doc
asVar = do
"* a variable bound at" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Range -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM (Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ LocalVar -> Name
localVar LocalVar
x)
shadowing :: LocalVar -> TCM Doc
shadowing :: LocalVar -> TCM Doc
shadowing (LocalVar _ _ []) = "shadowing"
shadowing _ = "in conflict with"
names :: [AbstractName] -> TCM Doc
names = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.vcat ([TCM Doc] -> TCM Doc)
-> ([AbstractName] -> [TCM Doc]) -> [AbstractName] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractName -> TCM Doc) -> [AbstractName] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbstractName -> TCM Doc
pName
modules :: [AbstractModule] -> TCM Doc
modules = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.vcat ([TCM Doc] -> TCM Doc)
-> ([AbstractModule] -> [TCM Doc]) -> [AbstractModule] -> TCM Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AbstractModule -> TCM Doc) -> [AbstractModule] -> [TCM Doc]
forall a b. (a -> b) -> [a] -> [b]
map AbstractModule -> TCM Doc
pMod
pKind :: KindOfName -> TCM Doc
pKind = \case
ConName -> "constructor"
FldName -> "record field"
PatternSynName -> "pattern synonym"
GeneralizeName -> "generalizable variable"
DisallowedGeneralizeName -> "generalizable variable from let open"
MacroName -> "macro name"
QuotableName -> "quotable name"
DataName -> "data type"
RecName -> "record type"
AxiomName -> "postulate"
PrimName -> "primitive function"
FunName -> "defined name"
OtherDefName -> "defined name"
pName :: AbstractName -> TCM Doc
pName :: AbstractName -> TCM Doc
pName a :: AbstractName
a = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.sep
[ "* a"
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> KindOfName -> TCM Doc
pKind (AbstractName -> KindOfName
anameKind AbstractName
a)
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TCP.text (QName -> String
forall a. Pretty a => a -> String
prettyShow (QName -> String) -> QName -> String
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a)
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "brought into scope by"
] TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$
Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 2 (Range -> WhyInScope -> TCM Doc
pWhy (Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName (QName -> Name) -> QName -> Name
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
a) (AbstractName -> WhyInScope
anameLineage AbstractName
a))
pMod :: AbstractModule -> TCM Doc
pMod :: AbstractModule -> TCM Doc
pMod a :: AbstractModule
a = [TCM Doc] -> TCM Doc
forall (m :: * -> *). Monad m => [m Doc] -> m Doc
TCP.sep
[ "* a module" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
TCP.text (ModuleName -> String
forall a. Pretty a => a -> String
prettyShow (ModuleName -> String) -> ModuleName -> String
forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a)
, Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 2 (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ "brought into scope by"
] TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$
Int -> TCM Doc -> TCM Doc
forall (m :: * -> *). Functor m => Int -> m Doc -> m Doc
TCP.nest 2 (Range -> WhyInScope -> TCM Doc
pWhy (Name -> Range
nameBindingSite (Name -> Range) -> Name -> Range
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName (QName -> Name) -> QName -> Name
forall a b. (a -> b) -> a -> b
$ ModuleName -> QName
mnameToQName (ModuleName -> QName) -> ModuleName -> QName
forall a b. (a -> b) -> a -> b
$ AbstractModule -> ModuleName
amodName AbstractModule
a) (AbstractModule -> WhyInScope
amodLineage AbstractModule
a))
pWhy :: Range -> WhyInScope -> TCM Doc
pWhy :: Range -> WhyInScope -> TCM Doc
pWhy r :: Range
r Defined = "- its definition at" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Range -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM Range
r
pWhy r :: Range
r (Opened (C.QName x :: Name
x) w :: WhyInScope
w) | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x = Range -> WhyInScope -> TCM Doc
pWhy Range
r WhyInScope
w
pWhy r :: Range
r (Opened m :: QName
m w :: WhyInScope
w) =
"- the opening of"
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM QName
m
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> "at"
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Range -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
m)
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$
Range -> WhyInScope -> TCM Doc
pWhy Range
r WhyInScope
w
pWhy r :: Range
r (Applied m :: QName
m w :: WhyInScope
w) =
"- the application of"
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> QName -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM QName
m
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> "at"
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Range -> TCM Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
TCP.prettyTCM (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
m)
TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.$$
Range -> WhyInScope -> TCM Doc
pWhy Range
r WhyInScope
w
prettyResponseContext
:: InteractionId
-> Bool
-> [ResponseContextEntry]
-> TCM Doc
prettyResponseContext :: InteractionId -> Bool -> [ResponseContextEntry] -> TCM Doc
prettyResponseContext ii :: InteractionId
ii rev :: Bool
rev ctx :: [ResponseContextEntry]
ctx = InteractionId -> TCM Doc -> TCM Doc
forall a. InteractionId -> TCM a -> TCM a
withInteractionId InteractionId
ii (TCM Doc -> TCM Doc) -> TCM Doc -> TCM Doc
forall a b. (a -> b) -> a -> b
$ do
Modality
mod <- (TCEnv -> Modality) -> TCMT IO Modality
forall (m :: * -> *) a. MonadTCEnv m => (TCEnv -> a) -> m a
asksTC TCEnv -> Modality
forall a. LensModality a => a -> Modality
getModality
Int -> [(String, Doc)] -> Doc
align 10 ([(String, Doc)] -> Doc)
-> ([[(String, Doc)]] -> [(String, Doc)])
-> [[(String, Doc)]]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(String, Doc)]] -> [(String, Doc)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[(String, Doc)]] -> [(String, Doc)])
-> ([[(String, Doc)]] -> [[(String, Doc)]])
-> [[(String, Doc)]]
-> [(String, Doc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> ([[(String, Doc)]] -> [[(String, Doc)]])
-> [[(String, Doc)]]
-> [[(String, Doc)]]
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
rev [[(String, Doc)]] -> [[(String, Doc)]]
forall a. [a] -> [a]
reverse ([[(String, Doc)]] -> Doc) -> TCMT IO [[(String, Doc)]] -> TCM Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[ResponseContextEntry]
-> (ResponseContextEntry -> TCMT IO [(String, Doc)])
-> TCMT IO [[(String, Doc)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ResponseContextEntry]
ctx ((ResponseContextEntry -> TCMT IO [(String, Doc)])
-> TCMT IO [[(String, Doc)]])
-> (ResponseContextEntry -> TCMT IO [(String, Doc)])
-> TCMT IO [[(String, Doc)]]
forall a b. (a -> b) -> a -> b
$ \ (ResponseContextEntry n :: Name
n x :: Name
x (Arg ai :: ArgInfo
ai expr :: Expr
expr) letv :: Maybe Expr
letv nis :: NameInScope
nis) -> do
let
prettyCtxName :: String
prettyCtxName :: String
prettyCtxName
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
| Name -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope Name
n NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
InScope = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
| Bool
otherwise = Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x
attribute :: String
attribute :: String
attribute = String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
c then "" else " "
where c :: String
c = Cohesion -> String
forall a. Pretty a => a -> String
prettyShow (ArgInfo -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion ArgInfo
ai)
extras :: [Doc]
extras :: [Doc]
extras = [[Doc]] -> [Doc]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Doc]] -> [Doc]) -> [[Doc]] -> [Doc]
forall a b. (a -> b) -> a -> b
$
[ [ "not in scope" | NameInScope -> NameInScope
forall a. LensInScope a => a -> NameInScope
isInScope NameInScope
nis NameInScope -> NameInScope -> Bool
forall a. Eq a => a -> a -> Bool
== NameInScope
C.NotInScope ]
, [ "erased" | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity ArgInfo
ai Quantity -> Quantity -> Bool
`moreQuantity` Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod ]
, [ "irrelevant" | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai Relevance -> Relevance -> Bool
`moreRelevant` Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod ]
, [ "instance" | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai ]
]
Doc
ty <- Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
Maybe Doc
maybeVal <- (Expr -> TCM Doc) -> Maybe Expr -> TCMT IO (Maybe Doc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Maybe Expr
letv
[(String, Doc)] -> TCMT IO [(String, Doc)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, Doc)] -> TCMT IO [(String, Doc)])
-> [(String, Doc)] -> TCMT IO [(String, Doc)]
forall a b. (a -> b) -> a -> b
$
[ (String
attribute String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
prettyCtxName, ":" Doc -> Doc -> Doc
<+> Doc
ty Doc -> Doc -> Doc
<+> ([Doc] -> Doc
parenSep [Doc]
extras)) ] [(String, Doc)] -> [(String, Doc)] -> [(String, Doc)]
forall a. [a] -> [a] -> [a]
++
[ (Name -> String
forall a. Pretty a => a -> String
prettyShow Name
x, "=" Doc -> Doc -> Doc
<+> Doc
val) | Doc
val <- Maybe Doc -> [Doc]
forall a. Maybe a -> [a]
maybeToList Maybe Doc
maybeVal ]
where
parenSep :: [Doc] -> Doc
parenSep :: [Doc] -> Doc
parenSep docs :: [Doc]
docs
| [Doc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc]
docs = Doc
forall a. Null a => a
empty
| Bool
otherwise = (" " Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
comma [Doc]
docs
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta norm :: Rewrite
norm ii :: InteractionId
ii = do
OutputConstraint Expr InteractionId
form <- Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
B.typeOfMeta Rewrite
norm InteractionId
ii
case OutputConstraint Expr InteractionId
form of
OfType _ e :: Expr
e -> Expr -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
_ -> OutputConstraint Expr InteractionId -> TCM Doc
forall c a (m :: * -> *).
(Pretty c, ToConcrete a c, MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr InteractionId
form
prettyTimed :: CPUTime -> Doc
prettyTimed :: CPUTime -> Doc
prettyTimed time :: CPUTime
time = "Time:" Doc -> Doc -> Doc
<+> CPUTime -> Doc
forall a. Pretty a => a -> Doc
pretty CPUTime
time