module Agda.Interaction.EmacsTop
( mimicGHCi
, namedMetaOf
, showGoals
, showInfoError
, explainWhyInScope
, prettyTypeOfMeta
) where
import Control.Monad
import Control.Monad.IO.Class ( MonadIO(..) )
import Control.Monad.State ( evalStateT )
import Control.Monad.Trans ( lift )
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 ( explainWhyInScope, getAllWarningsOfTCErr, 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.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 -> [Char] -> TCM () -> TCM ()
repl (IO () -> TCM ()
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ())
-> ([Lisp [Char]] -> IO ()) -> [Lisp [Char]] -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Lisp [Char] -> IO ()) -> [Lisp [Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Char] -> IO ()
putStrLn ([Char] -> IO ())
-> (Lisp [Char] -> [Char]) -> Lisp [Char] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lisp [Char] -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow) ([Lisp [Char]] -> TCM ())
-> (Response -> TCMT IO [Lisp [Char]]) -> InteractionOutputCallback
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response -> TCMT IO [Lisp [Char]]
lispifyResponse) [Char]
"Agda2> "
lispifyResponse :: Response -> TCM [Lisp String]
lispifyResponse :: Response -> TCMT IO [Lisp [Char]]
lispifyResponse (Resp_HighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile) =
(Lisp [Char] -> [Lisp [Char]] -> [Lisp [Char]]
forall a. a -> [a] -> [a]
:[]) (Lisp [Char] -> [Lisp [Char]])
-> TCMT IO (Lisp [Char]) -> TCMT IO [Lisp [Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO (Lisp [Char]) -> TCMT IO (Lisp [Char])
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (HighlightingInfo
-> RemoveTokenBasedHighlighting
-> HighlightingMethod
-> ModuleToSource
-> IO (Lisp [Char])
lispifyHighlightingInfo HighlightingInfo
info RemoveTokenBasedHighlighting
remove HighlightingMethod
method ModuleToSource
modFile)
lispifyResponse (Resp_DisplayInfo DisplayInfo
info) = DisplayInfo -> TCMT IO [Lisp [Char]]
lispifyDisplayInfo DisplayInfo
info
lispifyResponse (Resp_ClearHighlighting TokenBased
tokenBased) =
[Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-highlight-clear" Lisp [Char] -> [Lisp [Char]] -> [Lisp [Char]]
forall a. a -> [a] -> [a]
:
case TokenBased
tokenBased of
TokenBased
NotOnlyTokenBased -> []
TokenBased
TokenBased ->
[ Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (TokenBased -> Lisp [Char]
lispifyTokenBased TokenBased
tokenBased) ]
]
lispifyResponse Response
Resp_DoneAborting = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-abort-done" ] ]
lispifyResponse Response
Resp_DoneExiting = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-exit-done" ] ]
lispifyResponse Response
Resp_ClearRunningInfo = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Lisp [Char]
clearRunningInfo ]
lispifyResponse (Resp_RunningInfo Nat
n [Char]
s)
| Nat
n Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
1 = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Char] -> Lisp [Char]
displayRunningInfo [Char]
s ]
| Bool
otherwise = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [[Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-verbose", [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> [Char]
quote [Char]
s)] ]
lispifyResponse (Resp_Status Status
s)
= [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-status-action"
, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> [Char]
quote ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Maybe [Char]] -> [[Char]]
forall a. [Maybe a] -> [a]
catMaybes [Maybe [Char]
checked, Maybe [Char]
showImpl, Maybe [Char]
showIrr])
]
]
where
checked :: Maybe [Char]
checked = Bool -> [Char] -> Maybe [Char]
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sChecked Status
s) [Char]
"Checked"
showImpl :: Maybe [Char]
showImpl = Bool -> [Char] -> Maybe [Char]
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sShowImplicitArguments Status
s) [Char]
"ShowImplicit"
showIrr :: Maybe [Char]
showIrr = Bool -> [Char] -> Maybe [Char]
forall a. Bool -> a -> Maybe a
boolToMaybe (Status -> Bool
sShowIrrelevantArguments Status
s) [Char]
"ShowIrrelevant"
lispifyResponse (Resp_JumpToError [Char]
f Int32
p) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
3 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$
[Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-maybe-goto", Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [[Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> [Char]
quote [Char]
f), [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
".", [Char] -> Lisp [Char]
forall a. a -> Lisp a
A (Int32 -> [Char]
forall a. Show a => a -> [Char]
show Int32
p)] ]
]
lispifyResponse (Resp_InteractionPoints [InteractionId]
is) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
1 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$
[Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [[Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-goals-action", Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ (InteractionId -> Lisp [Char]) -> [InteractionId] -> [Lisp [Char]]
forall a b. (a -> b) -> [a] -> [b]
map InteractionId -> Lisp [Char]
showNumIId [InteractionId]
is]
]
lispifyResponse (Resp_GiveAction InteractionId
ii GiveResult
s)
= [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-give-action", InteractionId -> Lisp [Char]
showNumIId InteractionId
ii, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
s' ] ]
where
s' :: [Char]
s' = case GiveResult
s of
Give_String [Char]
str -> [Char] -> [Char]
quote [Char]
str
GiveResult
Give_Paren -> [Char]
"'paren"
GiveResult
Give_NoParen -> [Char]
"'no-paren"
lispifyResponse (Resp_MakeCase InteractionId
ii MakeCaseVariant
variant [[Char]]
pcs) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
2 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
cmd, Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ ([Char] -> Lisp [Char]) -> [[Char]] -> [Lisp [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char])
-> ([Char] -> [Char]) -> [Char] -> Lisp [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
quote) [[Char]]
pcs ] ]
where
cmd :: [Char]
cmd = case MakeCaseVariant
variant of
MakeCaseVariant
R.Function -> [Char]
"agda2-make-case-action"
MakeCaseVariant
R.ExtendedLambda -> [Char]
"agda2-make-case-action-extendlam"
lispifyResponse (Resp_SolveAll [(InteractionId, Expr)]
ps) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return
[ Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
2 (Lisp [Char] -> Lisp [Char]) -> Lisp [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$
[Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-solveAll-action", Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a
Q (Lisp [Char] -> Lisp [Char])
-> ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L ([Lisp [Char]] -> Lisp [Char]) -> [Lisp [Char]] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ ((InteractionId, Expr) -> [Lisp [Char]])
-> [(InteractionId, Expr)] -> [Lisp [Char]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (InteractionId, Expr) -> [Lisp [Char]]
forall {a}. Pretty a => (InteractionId, a) -> [Lisp [Char]]
prn [(InteractionId, Expr)]
ps ]
]
where
prn :: (InteractionId, a) -> [Lisp [Char]]
prn (InteractionId
ii,a
e)= [InteractionId -> Lisp [Char]
showNumIId InteractionId
ii, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
quote ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ a -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow a
e]
lispifyDisplayInfo :: DisplayInfo -> TCM [Lisp String]
lispifyDisplayInfo :: DisplayInfo -> TCMT IO [Lisp [Char]]
lispifyDisplayInfo DisplayInfo
info = case DisplayInfo
info of
Info_CompilationOk CompilerBackend
backend WarningsAndNonFatalErrors
ws -> do
[Char]
warnings <- [TCWarning] -> TCM [Char]
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
ws)
[Char]
errors <- [TCWarning] -> TCM [Char]
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
ws)
let
msg :: [Char]
msg = [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char]
"The module was successfully compiled with backend "
, CompilerBackend -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow CompilerBackend
backend
, [Char]
".\n"
]
([Char]
body, [Char]
_) = [Char] -> [Char] -> [Char] -> ([Char], [Char])
formatWarningsAndErrors [Char]
msg [Char]
warnings [Char]
errors
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format [Char]
body [Char]
"*Compilation result*"
Info_Constraints [OutputForm Expr Expr]
s -> do
Doc
doc <- [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (OutputForm Expr Expr -> TCMT IO Doc)
-> [OutputForm Expr Expr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm Expr Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
OutputForm Expr Expr -> m Doc
prettyTCM [OutputForm Expr Expr]
s
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Constraints*"
Info_AllGoalsWarnings Goals
ms WarningsAndNonFatalErrors
ws -> do
[Char]
goals <- Goals -> TCM [Char]
showGoals Goals
ms
[Char]
warnings <- [TCWarning] -> TCM [Char]
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
ws)
[Char]
errors <- [TCWarning] -> TCM [Char]
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
nonFatalErrors WarningsAndNonFatalErrors
ws)
let ([Char]
body, [Char]
title) = [Char] -> [Char] -> [Char] -> ([Char], [Char])
formatWarningsAndErrors [Char]
goals [Char]
warnings [Char]
errors
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format [Char]
body ([Char]
"*All" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
title [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"*")
Info_Auto [Char]
s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
format [Char]
s [Char]
"*Auto*"
Info_Error Info_Error
err -> do
[Char]
s <- Info_Error -> TCM [Char]
showInfoError Info_Error
err
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format [Char]
s [Char]
"*Error*"
Info_Time CPUTime
s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ CPUTime -> Doc
prettyTimed CPUTime
s) [Char]
"*Time*"
Info_NormalForm CommandState
state ComputeMode
cmode Maybe CPUTime
time Expr
expr -> do
Doc
exprDoc <- StateT CommandState (TCMT IO) Doc -> CommandState -> TCMT IO Doc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState (TCMT IO) 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
lbl :: [Char]
lbl | ComputeMode
cmode ComputeMode -> ComputeMode -> Bool
forall a. Eq a => a -> a -> Bool
== ComputeMode
HeadCompute = [Char]
"*Head Normal Form*"
| Bool
otherwise = [Char]
"*Normal Form*"
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
lbl
where
prettyExpr :: StateT CommandState (TCMT IO) Doc
prettyExpr = StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a. CommandM a -> CommandM a
localStateCommandM
(StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc)
-> StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
(TCMT IO Doc -> StateT CommandState (TCMT IO) Doc)
-> TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
B.atTopLevel
(TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
(TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (if ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
cmode then TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
(TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (ComputeMode -> Expr -> TCMT IO Doc
B.showComputed ComputeMode
cmode)
(Expr -> TCMT IO Doc) -> Expr -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Expr
expr
Info_InferredType CommandState
state Maybe CPUTime
time Expr
expr -> do
Doc
exprDoc <- StateT CommandState (TCMT IO) Doc -> CommandState -> TCMT IO Doc
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState (TCMT IO) 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
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Inferred Type*"
where
prettyExpr :: StateT CommandState (TCMT IO) Doc
prettyExpr = StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a. CommandM a -> CommandM a
localStateCommandM
(StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc)
-> StateT CommandState (TCMT IO) Doc
-> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall (m :: * -> *) a. Monad m => m a -> StateT CommandState m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
(TCMT IO Doc -> StateT CommandState (TCMT IO) Doc)
-> TCMT IO Doc -> StateT CommandState (TCMT IO) Doc
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
B.atTopLevel
(TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
TCP.prettyA
(Expr -> TCMT IO Doc) -> Expr -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Expr
expr
Info_ModuleContents [Name]
modules Telescope
tel [(Name, Type)]
types -> do
Doc
doc <- TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
localTCState (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ do
[([Char], Doc)]
typeDocs <- Telescope -> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
forall (m :: * -> *) a.
MonadAddContext m =>
Telescope -> m a -> m a
addContext Telescope
tel (TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)])
-> TCMT IO [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$ [(Name, Type)]
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], 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 ([Char], Doc))
-> TCMT IO [([Char], Doc)])
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$ \ (Name
x, Type
t) -> do
Doc
doc <- Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
([Char], Doc) -> TCMT IO ([Char], Doc)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
":" Doc -> Doc -> Doc
<+> Doc
doc)
Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat
[ Doc
"Modules"
, Nat -> Doc -> Doc
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t 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
, Doc
"Names"
, Nat -> Doc -> Doc
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Nat -> [([Char], Doc)] -> Doc
align Nat
10 [([Char], Doc)]
typeDocs
]
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Module contents*"
Info_SearchAbout [(Name, Type)]
hits [Char]
names -> do
[([Char], Doc)]
hitDocs <- [(Name, Type)]
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], 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 ([Char], Doc))
-> TCMT IO [([Char], Doc)])
-> ((Name, Type) -> TCMT IO ([Char], Doc))
-> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$ \ (Name
x, Type
t) -> do
Doc
doc <- Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t
([Char], Doc) -> TCMT IO ([Char], Doc)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
":" Doc -> Doc -> Doc
<+> Doc
doc)
let doc :: Doc
doc = Doc
"Definitions about" Doc -> Doc -> Doc
<+>
[Char] -> Doc
text ([Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
", " ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [[Char]]
words [Char]
names) Doc -> Doc -> Doc
$$ Nat -> Doc -> Doc
nest Nat
2 (Nat -> [([Char], Doc)] -> Doc
align Nat
10 [([Char], Doc)]
hitDocs)
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Search About*"
Info_WhyInScope WhyInScopeData
why -> do
Doc
doc <- WhyInScopeData -> TCMT IO Doc
forall (m :: * -> *). MonadPretty m => WhyInScopeData -> m Doc
explainWhyInScope WhyInScopeData
why
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Scope Info*"
Info_Context InteractionId
ii [ResponseContextEntry]
ctx -> do
Doc
doc <- TCMT IO Doc -> TCMT IO Doc
forall a. TCM a -> TCM a
localTCState (InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
prettyResponseContext InteractionId
ii Bool
False [ResponseContextEntry]
ctx)
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Context*"
DisplayInfo
Info_Intro_NotFound -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
format [Char]
"No introduction forms found." [Char]
"*Intro*"
Info_Intro_ConstructorUnknown [[Char]]
ss -> do
let doc :: Doc
doc = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
sep [ Doc
"Don't know which constructor to introduce of"
, let mkOr :: [[Char]] -> [Doc]
mkOr [] = []
mkOr [[Char]
x, [Char]
y] = [[Char] -> Doc
text [Char]
x Doc -> Doc -> Doc
<+> Doc
"or" Doc -> Doc -> Doc
<+> [Char] -> Doc
text [Char]
y]
mkOr ([Char]
x:[[Char]]
xs) = [Char] -> Doc
text [Char]
x Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: [[Char]] -> [Doc]
mkOr [[Char]]
xs
in Nat -> Doc -> Doc
nest Nat
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma ([[Char]] -> [Doc]
mkOr [[Char]]
ss)
]
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Intro*"
DisplayInfo
Info_Version -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
format ([Char]
"Agda version " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
versionWithCommitInfo) [Char]
"*Agda Version*"
Info_GoalSpecific InteractionId
ii GoalDisplayInfo
kind -> InteractionId -> GoalDisplayInfo -> TCMT IO [Lisp [Char]]
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo
kind
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String]
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCMT IO [Lisp [Char]]
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo
kind = TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. TCM a -> TCM a
localTCState (TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]])
-> TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a b. (a -> b) -> a -> b
$ InteractionId -> TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]])
-> TCMT IO [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a b. (a -> b) -> a -> b
$
case GoalDisplayInfo
kind of
Goal_HelperFunction OutputConstraint' Expr Expr
helperType -> do
Doc
doc <- TCMT IO Doc -> TCMT IO Doc
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ OutputConstraint' Expr Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint' Expr Expr
helperType
[Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ [Lisp [Char]] -> Lisp [Char]
forall a. [Lisp a] -> Lisp a
L [ [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"agda2-info-action-and-copy"
, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
quote [Char]
"*Helper function*"
, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
quote (Doc -> [Char]
render Doc
doc [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
, [Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"nil"
]
]
Goal_NormalForm ComputeMode
cmode Expr
expr -> do
Doc
doc <- ComputeMode -> Expr -> TCMT IO Doc
showComputed ComputeMode
cmode Expr
expr
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Normal Form*"
Goal_GoalType Rewrite
norm GoalTypeAux
aux [ResponseContextEntry]
ctx [IPBoundary' Expr]
bndry [OutputForm Expr Expr]
constraints -> do
Doc
ctxDoc <- InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
prettyResponseContext InteractionId
ii Bool
True [ResponseContextEntry]
ctx
Doc
goalDoc <- Rewrite -> InteractionId -> TCMT IO Doc
prettyTypeOfMeta Rewrite
norm InteractionId
ii
Doc
auxDoc <- case GoalTypeAux
aux of
GoalTypeAux
GoalOnly -> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
forall a. Null a => a
empty
GoalAndHave Expr
expr -> do
Doc
doc <- Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Have:" Doc -> Doc -> Doc
<+> Doc
doc
GoalAndElaboration Term
term -> do
Doc
doc <- Term -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Term -> m Doc
TCP.prettyTCM Term
term
Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Doc -> TCMT IO Doc) -> Doc -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ Doc
"Elaborates to:" Doc -> Doc -> Doc
<+> Doc
doc
let boundaryDoc :: [Doc]
boundaryDoc
| [IPBoundary' Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IPBoundary' Expr]
bndry = []
| Bool
otherwise = [ [Char] -> Doc
text ([Char] -> Doc) -> [Char] -> Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
delimiter [Char]
"Boundary"
, [Doc] -> Doc
forall (t :: * -> *). Foldable t => t 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 :: [TCMT IO Doc]
constraintsDoc
| [OutputForm Expr Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OutputForm Expr Expr]
constraints = []
| Bool
otherwise =
[ [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text ([Char] -> TCMT IO Doc) -> [Char] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
delimiter [Char]
"Constraints"
, [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$ (OutputForm Expr Expr -> TCMT IO Doc)
-> [OutputForm Expr Expr] -> [TCMT IO Doc]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm Expr Expr -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *).
MonadPretty m =>
OutputForm Expr Expr -> m Doc
prettyTCM [OutputForm Expr Expr]
constraints
]
Doc
doc <- [TCMT IO Doc] -> TCMT IO Doc
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m Doc) -> m Doc
TCP.vcat ([TCMT IO Doc] -> TCMT IO Doc) -> [TCMT IO Doc] -> TCMT IO Doc
forall a b. (a -> b) -> a -> b
$
[ TCMT IO Doc
"Goal:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
TCP.<+> Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
goalDoc
, Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
auxDoc
, Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
vcat [Doc]
boundaryDoc)
, [Char] -> TCMT IO Doc
forall (m :: * -> *). Applicative m => [Char] -> m Doc
TCP.text (Nat -> Char -> [Char]
forall a. Nat -> a -> [a]
replicate Nat
60 Char
'\x2014')
, Doc -> TCMT IO Doc
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc
ctxDoc
] [TCMT IO Doc] -> [TCMT IO Doc] -> [TCMT IO Doc]
forall a. [a] -> [a] -> [a]
++ [TCMT IO Doc]
constraintsDoc
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Goal type etc.*"
Goal_CurrentGoal Rewrite
norm -> do
Doc
doc <- Rewrite -> InteractionId -> TCMT IO Doc
prettyTypeOfMeta Rewrite
norm InteractionId
ii
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Current Goal*"
Goal_InferredType Expr
expr -> do
Doc
doc <- Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc -> [Char]
render Doc
doc) [Char]
"*Inferred Type*"
format :: String -> String -> TCM [Lisp String]
format :: [Char] -> [Char] -> TCMT IO [Lisp [Char]]
format [Char]
content [Char]
bufname = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Bool -> [Char] -> [Char] -> Lisp [Char]
display_info' Bool
False [Char]
bufname [Char]
content ]
lastTag :: Integer -> Lisp String -> Lisp String
lastTag :: Integer -> Lisp [Char] -> Lisp [Char]
lastTag Integer
n Lisp [Char]
r = Lisp [Char] -> Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a -> Lisp a
Cons (Lisp [Char] -> Lisp [Char] -> Lisp [Char]
forall a. Lisp a -> Lisp a -> Lisp a
Cons ([Char] -> Lisp [Char]
forall a. a -> Lisp a
A [Char]
"last") ([Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char]) -> [Char] -> Lisp [Char]
forall a b. (a -> b) -> a -> b
$ Integer -> [Char]
forall a. Show a => a -> [Char]
show Integer
n)) Lisp [Char]
r
showNumIId :: InteractionId -> Lisp String
showNumIId :: InteractionId -> Lisp [Char]
showNumIId = [Char] -> Lisp [Char]
forall a. a -> Lisp a
A ([Char] -> Lisp [Char])
-> (InteractionId -> [Char]) -> InteractionId -> Lisp [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> [Char]
forall a. Show a => a -> [Char]
show (Nat -> [Char])
-> (InteractionId -> Nat) -> InteractionId -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId -> Nat
interactionId
formatWarningsAndErrors :: String -> String -> String -> (String, String)
formatWarningsAndErrors :: [Char] -> [Char] -> [Char] -> ([Char], [Char])
formatWarningsAndErrors [Char]
g [Char]
w [Char]
e = ([Char]
body, [Char]
title)
where
isG :: Bool
isG = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
g
isW :: Bool
isW = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
w
isE :: Bool
isE = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
e
title :: [Char]
title = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Maybe [Char]] -> [[Char]]
forall a. [Maybe a] -> [a]
catMaybes
[ [Char]
" Goals" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
, [Char]
" Errors" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
, [Char]
" Warnings" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isW
, [Char]
" Done" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
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 :: [Char]
body = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Maybe [Char]] -> [[Char]]
forall a. [Maybe a] -> [a]
catMaybes
[ [Char]
g [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isG
, [Char] -> [Char]
delimiter [Char]
"Errors" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
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))
, [Char]
e [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard Bool
isE
, [Char] -> [Char]
delimiter [Char]
"Warnings" [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
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))
, [Char]
w [Char] -> Maybe () -> Maybe [Char]
forall a b. a -> Maybe b -> Maybe a
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 [Char]
showInfoError (Info_GenericError TCErr
err) = do
[Char]
e <- TCErr -> TCM [Char]
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
prettyError TCErr
err
[[Char]]
w <- [TCWarning] -> TCM [[Char]]
prettyTCWarnings' ([TCWarning] -> TCM [[Char]])
-> TCMT IO [TCWarning] -> TCM [[Char]]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCErr -> TCMT IO [TCWarning]
getAllWarningsOfTCErr TCErr
err
let errorMsg :: [Char]
errorMsg = if [[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
w
then [Char]
e
else [Char] -> [Char]
delimiter [Char]
"Error" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
e
let warningMsg :: [Char]
warningMsg = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
List.intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
delimiter [Char]
"Warning(s)"
[Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ([Char] -> Bool) -> [[Char]] -> [[Char]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([Char] -> Bool) -> [Char] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [[Char]]
w
[Char] -> TCM [Char]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
forall a b. (a -> b) -> a -> b
$ if [[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
w
then [Char]
errorMsg
else [Char]
errorMsg [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
warningMsg
showInfoError (Info_CompilationError [TCWarning]
warnings) = do
[Char]
s <- [TCWarning] -> TCM [Char]
prettyTCWarnings [TCWarning]
warnings
[Char] -> TCM [Char]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines
[ [Char]
"You need to fix the following errors before you can compile"
, [Char]
"the module:"
, [Char]
""
, [Char]
s
]
showInfoError (Info_HighlightingParseError InteractionId
ii) =
[Char] -> TCM [Char]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"Highlighting failed to parse expression in " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ InteractionId -> [Char]
forall a. Show a => a -> [Char]
show InteractionId
ii
showInfoError (Info_HighlightingScopeCheckError InteractionId
ii) =
[Char] -> TCM [Char]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> TCM [Char]) -> [Char] -> TCM [Char]
forall a b. (a -> b) -> a -> b
$ [Char]
"Highlighting failed to scope check expression in " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ InteractionId -> [Char]
forall a. Show a => a -> [Char]
show InteractionId
ii
prettyResponseContext
:: InteractionId
-> Bool
-> [ResponseContextEntry]
-> TCM Doc
prettyResponseContext :: InteractionId -> Bool -> [ResponseContextEntry] -> TCMT IO Doc
prettyResponseContext InteractionId
ii Bool
rev [ResponseContextEntry]
ctx = InteractionId -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *) a.
(MonadDebug m, MonadFail m, ReadTCState m, MonadError TCErr m,
MonadTCEnv m, MonadTrace m) =>
InteractionId -> m a -> m a
withInteractionId InteractionId
ii (TCMT IO Doc -> TCMT IO Doc) -> TCMT IO Doc -> TCMT IO 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
Nat -> [([Char], Doc)] -> Doc
align Nat
10 ([([Char], Doc)] -> Doc)
-> ([[([Char], Doc)]] -> [([Char], Doc)])
-> [[([Char], Doc)]]
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[([Char], Doc)]] -> [([Char], Doc)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[([Char], Doc)]] -> [([Char], Doc)])
-> ([[([Char], Doc)]] -> [[([Char], Doc)]])
-> [[([Char], Doc)]]
-> [([Char], Doc)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool
-> ([[([Char], Doc)]] -> [[([Char], Doc)]])
-> [[([Char], Doc)]]
-> [[([Char], Doc)]]
forall a. Bool -> (a -> a) -> a -> a
applyWhen Bool
rev [[([Char], Doc)]] -> [[([Char], Doc)]]
forall a. [a] -> [a]
reverse ([[([Char], Doc)]] -> Doc)
-> TCMT IO [[([Char], Doc)]] -> TCMT IO Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> do
[ResponseContextEntry]
-> (ResponseContextEntry -> TCMT IO [([Char], Doc)])
-> TCMT IO [[([Char], Doc)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [ResponseContextEntry]
ctx ((ResponseContextEntry -> TCMT IO [([Char], Doc)])
-> TCMT IO [[([Char], Doc)]])
-> (ResponseContextEntry -> TCMT IO [([Char], Doc)])
-> TCMT IO [[([Char], Doc)]]
forall a b. (a -> b) -> a -> b
$ \ (ResponseContextEntry Name
n Name
x (Arg ArgInfo
ai Expr
expr) Maybe Expr
letv NameInScope
nis) -> do
let
prettyCtxName :: String
prettyCtxName :: [Char]
prettyCtxName
| Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
x = Name -> [Char]
forall a. Pretty a => a -> [Char]
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 -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
n [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
| Bool
otherwise = Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x
attribute :: String
attribute :: [Char]
attribute = [Char]
c [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ if [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
c then [Char]
"" else [Char]
" "
where c :: [Char]
c = Cohesion -> [Char]
forall a. Pretty a => a -> [Char]
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
$
[ [ Doc
"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 ]
, [ Doc
"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 ]
, [ Doc
"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 ]
, [ Doc
"instance" | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai ]
]
Doc
ty <- Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
expr
Maybe Doc
maybeVal <- (Expr -> TCMT IO Doc) -> Maybe Expr -> TCMT IO (Maybe Doc)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Maybe a -> f (Maybe b)
traverse Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Maybe Expr
letv
[([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([([Char], Doc)] -> TCMT IO [([Char], Doc)])
-> [([Char], Doc)] -> TCMT IO [([Char], Doc)]
forall a b. (a -> b) -> a -> b
$
([Char]
attribute [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
prettyCtxName, Doc
":" Doc -> Doc -> Doc
<+> Doc
ty Doc -> Doc -> Doc
<+> ([Doc] -> Doc
parenSep [Doc]
extras)) ([Char], Doc) -> [([Char], Doc)] -> [([Char], Doc)]
forall a. a -> [a] -> [a]
:
[ (Name -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Name
x, Doc
"=" 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 [Doc]
docs
| [Doc] -> Bool
forall a. [a] -> 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 -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
forall (t :: * -> *). Foldable t => Doc -> t Doc -> [Doc]
punctuate Doc
comma [Doc]
docs
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCMT IO Doc
prettyTypeOfMeta Rewrite
norm 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 InteractionId
_ Expr
e -> Expr -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop Expr
e
OutputConstraint Expr InteractionId
_ -> OutputConstraint Expr InteractionId -> TCMT IO Doc
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m Doc
prettyATop OutputConstraint Expr InteractionId
form
prettyTimed :: CPUTime -> Doc
prettyTimed :: CPUTime -> Doc
prettyTimed CPUTime
time = Doc
"Time:" Doc -> Doc -> Doc
<+> CPUTime -> Doc
forall a. Pretty a => a -> Doc
pretty CPUTime
time