{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Interaction.EmacsTop
( mimicGHCi
, namedMetaOf
, showGoals
, showInfoError
, explainWhyInScope
, prettyResponseContext
, 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.Common.Pretty
import Agda.Syntax.Abstract.Pretty (prettyATop)
import Agda.Syntax.Concrete as C
import Agda.TypeChecking.Errors ( explainWhyInScope, getAllWarningsOfTCErr, renderError, verbalize )
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Pretty (prettyTCM)
import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings)
import Agda.TypeChecking.Monad
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.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_boot TCErr TCWarning WarningsAndNonFatalErrors
-> TCMT IO [Lisp [Char]])
-> InteractionOutputCallback
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< Response_boot TCErr TCWarning WarningsAndNonFatalErrors
-> TCMT IO [Lisp [Char]]
lispifyResponse) [Char]
"Agda2> "
lispifyResponse :: Response -> TCM [Lisp String]
lispifyResponse :: Response_boot TCErr TCWarning WarningsAndNonFatalErrors
-> 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_boot TCErr TCWarning WarningsAndNonFatalErrors
info) = DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> TCMT IO [Lisp [Char]]
lispifyDisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
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_boot TCErr TCWarning WarningsAndNonFatalErrors
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_boot TCErr TCWarning WarningsAndNonFatalErrors
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_boot TCErr TCWarning WarningsAndNonFatalErrors
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]
lispifyResponse (Resp_Mimer InteractionId
ii Maybe [Char]
msol) = [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Lisp [Char]] -> TCMT IO [Lisp [Char]])
-> [Lisp [Char]] -> TCMT IO [Lisp [Char]]
forall a b. (a -> b) -> a -> b
$ case Maybe [Char]
msol of
Maybe [Char]
Nothing ->
[ 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-info-action", [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]
"*Mimer*", [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]
"No solution found" ]
]
Just [Char]
str ->
[ 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-solve-action", 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]
str ]
]
lispifyDisplayInfo :: DisplayInfo -> TCM [Lisp String]
lispifyDisplayInfo :: DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
-> TCMT IO [Lisp [Char]]
lispifyDisplayInfo DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info = case DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
info of
Info_CompilationOk CompilerBackend
backend WarningsAndNonFatalErrors
ws -> do
warnings <- [TCWarning] -> TCM [Char]
prettyTCWarnings (WarningsAndNonFatalErrors -> [TCWarning]
tcWarnings WarningsAndNonFatalErrors
ws)
errors <- prettyTCWarnings (nonFatalErrors ws)
let
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"
]
(body, _) = formatWarningsAndErrors msg warnings errors
format body "*Compilation result*"
Info_Constraints [OutputForm_boot TCErr Expr Expr]
s -> do
doc <- [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m (Doc Aspects)) -> m (Doc Aspects)
TCP.vcat ([TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects))
-> [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ (OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects))
-> [OutputForm_boot TCErr Expr Expr] -> [TCMT IO (Doc Aspects)]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
OutputForm_boot TCErr Expr Expr -> m (Doc Aspects)
prettyTCM [OutputForm_boot TCErr Expr Expr]
s
format (render doc) "*Constraints*"
Info_AllGoalsWarnings Goals_boot TCErr
ms WarningsAndNonFatalErrors
ws -> do
goals <- Goals_boot TCErr -> TCM [Char]
showGoals Goals_boot TCErr
ms
warnings <- prettyTCWarnings (tcWarnings ws)
errors <- prettyTCWarnings (nonFatalErrors ws)
let (body, title) = formatWarningsAndErrors goals warnings errors
format body ("*All" ++ title ++ "*")
Info_Auto [Char]
s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
format [Char]
s [Char]
"*Auto*"
Info_Error Info_Error_boot TCErr TCWarning
err -> do
s <- Info_Error_boot TCErr TCWarning -> TCM [Char]
showInfoError Info_Error_boot TCErr TCWarning
err
format s "*Error*"
Info_Time CPUTime
s -> [Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render (Doc Aspects -> [Char]) -> Doc Aspects -> [Char]
forall a b. (a -> b) -> a -> b
$ CPUTime -> Doc Aspects
prettyTimed CPUTime
s) [Char]
"*Time*"
Info_NormalForm CommandState
state ComputeMode
cmode Maybe CPUTime
time Expr
expr -> do
exprDoc <- StateT CommandState (TCMT IO) (Doc Aspects)
-> CommandState -> TCMT IO (Doc Aspects)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState (TCMT IO) (Doc Aspects)
prettyExpr CommandState
state
let doc = Doc Aspects
-> (CPUTime -> Doc Aspects) -> Maybe CPUTime -> Doc Aspects
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc Aspects
forall a. Null a => a
empty CPUTime -> Doc Aspects
prettyTimed Maybe CPUTime
time Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
$$ Doc Aspects
exprDoc
lbl | ComputeMode
cmode ComputeMode -> ComputeMode -> Bool
forall a. Eq a => a -> a -> Bool
== ComputeMode
HeadCompute = [Char]
"*Head Normal Form*"
| Bool
otherwise = [Char]
"*Normal Form*"
format (render doc) lbl
where
prettyExpr :: StateT CommandState (TCMT IO) (Doc Aspects)
prettyExpr = StateT CommandState (TCMT IO) (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
forall a. CommandM a -> CommandM a
localStateCommandM
(StateT CommandState (TCMT IO) (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects))
-> StateT CommandState (TCMT IO) (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
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 Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects))
-> TCMT IO (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a. TCM a -> TCM a
B.atTopLevel
(TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
allowNonTerminatingReductions
(TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ (if ComputeMode -> Bool
computeIgnoreAbstract ComputeMode
cmode then TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode else TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
inConcreteMode)
(TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ (ComputeMode -> Expr -> TCMT IO (Doc Aspects)
B.showComputed ComputeMode
cmode)
(Expr -> TCMT IO (Doc Aspects)) -> Expr -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Expr
expr
Info_InferredType CommandState
state Maybe CPUTime
time Expr
expr -> do
exprDoc <- StateT CommandState (TCMT IO) (Doc Aspects)
-> CommandState -> TCMT IO (Doc Aspects)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT CommandState (TCMT IO) (Doc Aspects)
prettyExpr CommandState
state
let doc = Doc Aspects
-> (CPUTime -> Doc Aspects) -> Maybe CPUTime -> Doc Aspects
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc Aspects
forall a. Null a => a
empty CPUTime -> Doc Aspects
prettyTimed Maybe CPUTime
time Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
$$ Doc Aspects
exprDoc
format (render doc) "*Inferred Type*"
where
prettyExpr :: StateT CommandState (TCMT IO) (Doc Aspects)
prettyExpr = StateT CommandState (TCMT IO) (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
forall a. CommandM a -> CommandM a
localStateCommandM
(StateT CommandState (TCMT IO) (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects))
-> StateT CommandState (TCMT IO) (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
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 Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects))
-> TCMT IO (Doc Aspects)
-> StateT CommandState (TCMT IO) (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a. TCM a -> TCM a
B.atTopLevel
(TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
TCP.prettyA
(Expr -> TCMT IO (Doc Aspects)) -> Expr -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ Expr
expr
Info_ModuleContents [Name]
modules Telescope
tel [(Name, Type)]
types -> do
doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a. TCM a -> TCM a
localTCState (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ do
typeDocs <- Telescope
-> TCMT IO [([Char], Doc Aspects)]
-> TCMT IO [([Char], Doc Aspects)]
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 Aspects)]
-> TCMT IO [([Char], Doc Aspects)])
-> TCMT IO [([Char], Doc Aspects)]
-> TCMT IO [([Char], Doc Aspects)]
forall a b. (a -> b) -> a -> b
$ [(Name, Type)]
-> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
-> TCMT IO [([Char], Doc Aspects)]
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 Aspects))
-> TCMT IO [([Char], Doc Aspects)])
-> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
-> TCMT IO [([Char], Doc Aspects)]
forall a b. (a -> b) -> a -> b
$ \ (Name
x, Type
t) -> do
doc <- Type -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Type -> m (Doc Aspects)
prettyTCM Type
t
return (prettyShow x, ":" <+> doc)
return $ vcat
[ "Modules"
, nest 2 $ vcat $ map pretty modules
, "Names"
, nest 2 $ align 10 typeDocs
]
format (render doc) "*Module contents*"
Info_SearchAbout [(Name, Type)]
hits [Char]
names -> do
hitDocs <- [(Name, Type)]
-> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
-> TCMT IO [([Char], Doc Aspects)]
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 Aspects))
-> TCMT IO [([Char], Doc Aspects)])
-> ((Name, Type) -> TCMT IO ([Char], Doc Aspects))
-> TCMT IO [([Char], Doc Aspects)]
forall a b. (a -> b) -> a -> b
$ \ (Name
x, Type
t) -> do
doc <- Type -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Type -> m (Doc Aspects)
prettyTCM Type
t
return (prettyShow x, ":" <+> doc)
let doc = Doc Aspects
"Definitions about" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+>
[Char] -> Doc Aspects
forall a. [Char] -> Doc a
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 Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
$$ Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Nat -> [([Char], Doc Aspects)] -> Doc Aspects
align Nat
10 [([Char], Doc Aspects)]
hitDocs)
format (render doc) "*Search About*"
Info_WhyInScope WhyInScopeData
why -> do
doc <- WhyInScopeData -> TCMT IO (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
WhyInScopeData -> m (Doc Aspects)
explainWhyInScope WhyInScopeData
why
format (render doc) "*Scope Info*"
Info_Context InteractionId
ii [ResponseContextEntry]
ctx -> do
doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a. TCM a -> TCM a
localTCState (InteractionId
-> Bool -> [ResponseContextEntry] -> TCMT IO (Doc Aspects)
prettyResponseContext InteractionId
ii Bool
False [ResponseContextEntry]
ctx)
format (render doc) "*Context*"
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
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 Aspects
doc = [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
sep [ Doc Aspects
"Don't know which constructor to introduce of"
, let mkOr :: [[Char]] -> [Doc a]
mkOr [] = []
mkOr [[Char]
x, [Char]
y] = [[Char] -> Doc a
forall a. [Char] -> Doc a
text [Char]
x Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> Doc a
"or" Doc a -> Doc a -> Doc a
forall a. Doc a -> Doc a -> Doc a
<+> [Char] -> Doc a
forall a. [Char] -> Doc a
text [Char]
y]
mkOr ([Char]
x:[[Char]]
xs) = [Char] -> Doc a
forall a. [Char] -> Doc a
text [Char]
x Doc a -> [Doc a] -> [Doc a]
forall a. a -> [a] -> [a]
: [[Char]] -> [Doc a]
mkOr [[Char]]
xs
in Nat -> Doc Aspects -> Doc Aspects
forall a. Nat -> Doc a -> Doc a
nest Nat
2 (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall (t :: * -> *).
Foldable t =>
Doc Aspects -> t (Doc Aspects) -> [Doc Aspects]
punctuate Doc Aspects
comma ([[Char]] -> [Doc Aspects]
forall {a}. [[Char]] -> [Doc a]
mkOr [[Char]]
ss)
]
[Char] -> [Char] -> TCMT IO [Lisp [Char]]
format (Doc Aspects -> [Char]
forall a. Doc a -> [Char]
render Doc Aspects
doc) [Char]
"*Intro*"
DisplayInfo_boot TCErr TCWarning WarningsAndNonFatalErrors
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_boot TCErr
kind -> InteractionId
-> GoalDisplayInfo_boot TCErr -> TCMT IO [Lisp [Char]]
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo_boot TCErr
kind
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String]
lispifyGoalSpecificDisplayInfo :: InteractionId
-> GoalDisplayInfo_boot TCErr -> TCMT IO [Lisp [Char]]
lispifyGoalSpecificDisplayInfo InteractionId
ii GoalDisplayInfo_boot TCErr
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_boot TCErr
kind of
Goal_HelperFunction OutputConstraint' Expr Expr
helperType -> do
doc <- TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ OutputConstraint' Expr Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop OutputConstraint' Expr Expr
helperType
return [ L [ A "agda2-info-action-and-copy"
, A $ quote "*Helper function*"
, A $ quote (render doc ++ "\n")
, A "nil"
]
]
Goal_NormalForm ComputeMode
cmode Expr
expr -> do
doc <- ComputeMode -> Expr -> TCMT IO (Doc Aspects)
showComputed ComputeMode
cmode Expr
expr
format (render doc) "*Normal Form*"
Goal_GoalType Rewrite
norm GoalTypeAux
aux [ResponseContextEntry]
ctx [IPFace' Expr]
bndry [OutputForm_boot TCErr Expr Expr]
constraints -> do
ctxDoc <- InteractionId
-> Bool -> [ResponseContextEntry] -> TCMT IO (Doc Aspects)
prettyResponseContext InteractionId
ii Bool
True [ResponseContextEntry]
ctx
goalDoc <- prettyTypeOfMeta norm ii
let boundaryDoc [Char]
hd [a]
bndry
| [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
bndry = []
| Bool
otherwise = [ [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
delimiter [Char]
hd
, [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
vcat ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ (a -> Doc Aspects) -> [a] -> [Doc Aspects]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty [a]
bndry
]
auxDoc <- case aux of
GoalTypeAux
GoalOnly -> Doc Aspects -> TCMT IO (Doc Aspects)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Doc Aspects
forall a. Null a => a
empty
GoalAndHave Expr
expr [IPFace' Expr]
bndry -> do
doc <- Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop Expr
expr
return $ ("Have:" <+> doc) $$ vcat (boundaryDoc ("Boundary (actual)") bndry)
GoalAndElaboration Term
term -> do
doc <- Term -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *). MonadPretty m => Term -> m (Doc Aspects)
TCP.prettyTCM Term
term
return $ "Elaborates to:" <+> doc
let constraintsDoc
| [OutputForm_boot TCErr Expr Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OutputForm_boot TCErr Expr Expr]
constraints = []
| Bool
otherwise =
[ [Char] -> TCMT IO (Doc Aspects)
forall (m :: * -> *). Applicative m => [Char] -> m (Doc Aspects)
TCP.text ([Char] -> TCMT IO (Doc Aspects))
-> [Char] -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char]
delimiter [Char]
"Constraints"
, [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
forall (m :: * -> *) (t :: * -> *).
(Applicative m, Foldable t) =>
t (m (Doc Aspects)) -> m (Doc Aspects)
TCP.vcat ([TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects))
-> [TCMT IO (Doc Aspects)] -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ (OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects))
-> [OutputForm_boot TCErr Expr Expr] -> [TCMT IO (Doc Aspects)]
forall a b. (a -> b) -> [a] -> [b]
map OutputForm_boot TCErr Expr Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(PrettyTCM a, MonadPretty m) =>
a -> m (Doc Aspects)
forall (m :: * -> *).
MonadPretty m =>
OutputForm_boot TCErr Expr Expr -> m (Doc Aspects)
prettyTCM [OutputForm_boot TCErr Expr Expr]
constraints
]
doc <- TCP.vcat $
[ "Goal:" TCP.<+> return goalDoc
, return (vcat (boundaryDoc "Boundary (wanted)" bndry))
, return auxDoc
, TCP.text (replicate 60 '\x2014')
, return ctxDoc
] ++ constraintsDoc
format (render doc) "*Goal type etc.*"
Goal_CurrentGoal Rewrite
norm -> do
doc <- Rewrite -> InteractionId -> TCMT IO (Doc Aspects)
prettyTypeOfMeta Rewrite
norm InteractionId
ii
format (render doc) "*Current Goal*"
Goal_InferredType Expr
expr -> do
doc <- Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop Expr
expr
format (render doc) "*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]
"Error" [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_boot TCErr TCWarning -> TCM [Char]
showInfoError (Info_GenericError TCErr
err) = do
e <- TCErr -> TCM [Char]
forall (tcm :: * -> *). MonadTCM tcm => TCErr -> tcm [Char]
renderError TCErr
err
w <- prettyTCWarnings =<< getAllWarningsOfTCErr err
let (body, _) = formatWarningsAndErrors "" w e
return body
showInfoError (Info_CompilationError [TCWarning]
warnings) = do
s <- [TCWarning] -> TCM [Char]
prettyTCWarnings [TCWarning]
warnings
return $ unlines
[ "You need to fix the following errors before you can compile the module:"
, ""
, 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 Aspects)
prettyResponseContext InteractionId
ii Bool
rev [ResponseContextEntry]
ctx = InteractionId -> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
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 Aspects) -> TCMT IO (Doc Aspects))
-> TCMT IO (Doc Aspects) -> TCMT IO (Doc Aspects)
forall a b. (a -> b) -> a -> b
$ do
mod <- TCMT IO Modality
forall (m :: * -> *). MonadTCEnv m => m Modality
currentModality
align 10 . concat . applyWhen rev reverse <$> do
forM ctx $ \ (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 Aspects]
extras = [[Doc Aspects]] -> [Doc Aspects]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Doc Aspects]] -> [Doc Aspects])
-> [[Doc Aspects]] -> [Doc Aspects]
forall a b. (a -> b) -> a -> b
$
[ [ Doc Aspects
"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 Aspects
"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 ]
, [ [Char] -> Doc Aspects
forall a. [Char] -> Doc a
text ([Char] -> Doc Aspects) -> [Char] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Relevance -> [Char]
forall a. Verbalize a => a -> [Char]
verbalize Relevance
r
| let r :: Relevance
r = Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod Relevance -> Relevance -> Relevance
`inverseComposeRelevance` ArgInfo -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance ArgInfo
ai
, Relevance
r Relevance -> Relevance -> Bool
forall a. Eq a => a -> a -> Bool
/= Relevance
Relevant ]
, [ Doc Aspects
"instance" | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
isInstance ArgInfo
ai ]
]
ty <- Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop Expr
expr
maybeVal <- traverse prettyATop letv
return $
(attribute ++ prettyCtxName, ":" <+> ty <+> (parenSep extras)) :
[ (prettyShow x, "=" <+> val) | val <- maybeToList maybeVal ]
where
parenSep :: [Doc] -> Doc
parenSep :: [Doc Aspects] -> Doc Aspects
parenSep [Doc Aspects]
docs
| [Doc Aspects] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Doc Aspects]
docs = Doc Aspects
forall a. Null a => a
empty
| Bool
otherwise = (Doc Aspects
" " Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+>) (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> Doc Aspects
parens (Doc Aspects -> Doc Aspects) -> Doc Aspects -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ [Doc Aspects] -> Doc Aspects
forall (t :: * -> *). Foldable t => t (Doc Aspects) -> Doc Aspects
fsep ([Doc Aspects] -> Doc Aspects) -> [Doc Aspects] -> Doc Aspects
forall a b. (a -> b) -> a -> b
$ Doc Aspects -> [Doc Aspects] -> [Doc Aspects]
forall (t :: * -> *).
Foldable t =>
Doc Aspects -> t (Doc Aspects) -> [Doc Aspects]
punctuate Doc Aspects
comma [Doc Aspects]
docs
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCMT IO (Doc Aspects)
prettyTypeOfMeta Rewrite
norm InteractionId
ii = do
form <- Rewrite
-> InteractionId -> TCM (OutputConstraint Expr InteractionId)
B.typeOfMeta Rewrite
norm InteractionId
ii
case form of
OfType InteractionId
_ Expr
e -> Expr -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop Expr
e
OutputConstraint Expr InteractionId
_ -> OutputConstraint Expr InteractionId -> TCMT IO (Doc Aspects)
forall a (m :: * -> *).
(ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
a -> m (Doc Aspects)
prettyATop OutputConstraint Expr InteractionId
form
prettyTimed :: CPUTime -> Doc
prettyTimed :: CPUTime -> Doc Aspects
prettyTimed CPUTime
time = Doc Aspects
"Time:" Doc Aspects -> Doc Aspects -> Doc Aspects
forall a. Doc a -> Doc a -> Doc a
<+> CPUTime -> Doc Aspects
forall a. Pretty a => a -> Doc Aspects
pretty CPUTime
time