{-# LANGUAGE CPP #-}
module Agda.Convert where
import Agda.IR (FromAgda (..))
import qualified Agda.IR as IR
import Agda.Interaction.Base
import Agda.Interaction.BasicOps as B
import Agda.Interaction.EmacsCommand (Lisp)
import Agda.Interaction.EmacsTop (showInfoError)
import Agda.Interaction.Highlighting.Common (chooseHighlightingMethod, toAtoms)
import Agda.Interaction.Highlighting.Precise (Aspects (..), DefinitionSite (..), HighlightingInfo, TokenBased (..))
import qualified Agda.Interaction.Highlighting.Range as Highlighting
#if MIN_VERSION_Agda(2,8,0)
import Agda.Interaction.Command (localStateCommandM)
import Agda.TypeChecking.Monad.Base (topLevelModuleFilePath)
#else
import Agda.Interaction.InteractionTop (localStateCommandM)
#endif
#if MIN_VERSION_Agda(2,7,0)
import Agda.Interaction.Output ( OutputConstraint )
#endif
import Agda.Interaction.Response as R
import Agda.Syntax.Abstract as A
import Agda.Syntax.Abstract.Pretty (prettyATop)
import Agda.Syntax.Common
import Agda.Syntax.Concrete as C
import Agda.Syntax.Internal (alwaysUnblock)
import Agda.Syntax.Position (HasRange (getRange), Range, noRange)
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Errors (explainWhyInScope, getAllWarningsOfTCErr, prettyError)
import Agda.TypeChecking.Monad hiding (Function)
import Agda.TypeChecking.Monad.MetaVars (withInteractionId)
import Agda.TypeChecking.Pretty (prettyTCM)
import qualified Agda.TypeChecking.Pretty as TCP
import Agda.TypeChecking.Pretty.Warning (filterTCWarnings, prettyTCWarnings, prettyTCWarnings')
import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors (..))
import Agda.Utils.FileName (filePath)
import Agda.Utils.Function (applyWhen)
import Agda.Utils.IO.TempFile (writeToTempFile)
import Agda.Utils.Impossible (__IMPOSSIBLE__)
import Agda.Utils.Maybe (catMaybes)
import Agda.Utils.Null (empty)
import Agda.Utils.RangeMap (IsBasicRangeMap (toList))
import Agda.Utils.String (delimiter)
import Agda.Utils.Time (CPUTime)
import Agda.VersionCommit (versionWithCommitInfo)
import Control.Monad
import Control.Monad.State hiding (state)
import qualified Data.Aeson as JSON
import qualified Data.ByteString.Lazy.Char8 as BS8
import qualified Data.List as List
import qualified Data.Map as Map
import Data.String (IsString)
import Render (Block (..), Inlines, Render (..), renderATop)
import qualified Render
import Agda.Syntax.Common.Pretty hiding (render)
import qualified Prettyprinter
responseAbbr :: (IsString a) => Response -> a
responseAbbr res = case res of
Resp_HighlightingInfo {} -> "Resp_HighlightingInfo"
Resp_Status {} -> "Resp_Status"
Resp_JumpToError {} -> "Resp_JumpToError"
Resp_InteractionPoints {} -> "Resp_InteractionPoints"
Resp_GiveAction {} -> "Resp_GiveAction"
Resp_MakeCase {} -> "Resp_MakeCase"
Resp_SolveAll {} -> "Resp_SolveAll"
#if MIN_VERSION_Agda(2,7,0)
Resp_Mimer {} -> "Resp_Mimer"
#endif
Resp_DisplayInfo {} -> "Resp_DisplayInfo"
Resp_RunningInfo {} -> "Resp_RunningInfo"
Resp_ClearRunningInfo {} -> "Resp_ClearRunningInfo"
Resp_ClearHighlighting {} -> "Resp_ClearHighlighting"
Resp_DoneAborting {} -> "Resp_DoneAborting"
Resp_DoneExiting {} -> "Resp_DoneExiting"
----------------------------------
serialize :: Lisp String -> String
serialize = show . pretty
fromResponse :: Response -> TCM IR.Response
fromResponse (Resp_HighlightingInfo info remove method modFile) =
fromHighlightingInfo info remove method modFile
fromResponse (Resp_DisplayInfo info) = IR.ResponseDisplayInfo <$> fromDisplayInfo info
fromResponse (Resp_ClearHighlighting TokenBased) = return IR.ResponseClearHighlightingTokenBased
fromResponse (Resp_ClearHighlighting NotOnlyTokenBased) = return IR.ResponseClearHighlightingNotOnlyTokenBased
fromResponse Resp_DoneAborting = return IR.ResponseDoneAborting
fromResponse Resp_DoneExiting = return IR.ResponseDoneExiting
fromResponse Resp_ClearRunningInfo = return IR.ResponseClearRunningInfo
fromResponse (Resp_RunningInfo n s) = return $ IR.ResponseRunningInfo n s
fromResponse (Resp_Status s) = return $ IR.ResponseStatus (sChecked s) (sShowImplicitArguments s)
fromResponse (Resp_JumpToError f p) = return $ IR.ResponseJumpToError f (fromIntegral p)
fromResponse (Resp_InteractionPoints is) =
return $ IR.ResponseInteractionPoints (fmap interactionId is)
fromResponse (Resp_GiveAction (InteractionId i) giveAction) =
return $ IR.ResponseGiveAction i (fromAgda giveAction)
fromResponse (Resp_MakeCase _ Function pcs) = return $ IR.ResponseMakeCaseFunction pcs
fromResponse (Resp_MakeCase _ ExtendedLambda pcs) = return $ IR.ResponseMakeCaseExtendedLambda pcs
#if MIN_VERSION_Agda(2,7,0)
fromResponse (Resp_Mimer (InteractionId i) s) = return $ IR.ResponseMimer i s
#endif
fromResponse (Resp_SolveAll ps) = return $ IR.ResponseSolveAll (fmap prn ps)
where
prn (InteractionId i, e) = (i, prettyShow e)
fromHighlightingInfo ::
HighlightingInfo ->
RemoveTokenBasedHighlighting ->
HighlightingMethod ->
ModuleToSource ->
TCM IR.Response
fromHighlightingInfo h remove method modFile =
case chooseHighlightingMethod h method of
Direct -> return $ IR.ResponseHighlightingInfoDirect info
Indirect -> IR.ResponseHighlightingInfoIndirect <$> indirect
where
fromAspects ::
(Highlighting.Range, Aspects) ->
IR.HighlightingInfo
fromAspects (range, aspects) =
IR.HighlightingInfo
(Highlighting.from range)
(Highlighting.to range)
(toAtoms aspects)
(tokenBased aspects == TokenBased)
(note aspects)
(defSite <$> definitionSite aspects)
where
defSite (DefinitionSite moduleName offset _ _) =
#if MIN_VERSION_Agda(2,8,0)
(filePath (topLevelModuleFilePath modFile moduleName), offset)
#else
(filePath (Map.findWithDefault __IMPOSSIBLE__ moduleName modFile), offset)
#endif
infos :: [IR.HighlightingInfo]
infos = fmap fromAspects (toList h)
keepHighlighting :: Bool
keepHighlighting =
case remove of
RemoveHighlighting -> False
KeepHighlighting -> True
info :: IR.HighlightingInfos
info = IR.HighlightingInfos keepHighlighting infos
indirect :: TCM FilePath
indirect = liftIO $ writeToTempFile (BS8.unpack (JSON.encode info))
fromDisplayInfo :: DisplayInfo -> TCM IR.DisplayInfo
fromDisplayInfo = \case
Info_CompilationOk _ ws -> do
-- filter
#if MIN_VERSION_Agda(2,8,0)
filteredWarnings <- filterTCWarnings (tcWarnings ws)
filteredErrors <- filterTCWarnings (nonFatalErrors ws)
#else
let filteredWarnings = filterTCWarnings (tcWarnings ws)
let filteredErrors = filterTCWarnings (nonFatalErrors ws)
#endif
-- serializes
warnings <- mapM prettyTCM filteredWarnings
errors <- mapM prettyTCM filteredErrors
return $ IR.DisplayInfoCompilationOk (fmap show warnings) (fmap show errors)
Info_Constraints s -> do
-- constraints <- forM s $ \e -> do
-- rendered <- renderTCM e
-- let raw = show (pretty e)
-- return $ Unlabeled rendered (Just raw)
-- return $ IR.DisplayInfoGeneric "Constraints" constraints
return $ IR.DisplayInfoGeneric "Constraints" [Unlabeled (Render.text $ show $ vcat $ fmap pretty s) Nothing Nothing]
Info_AllGoalsWarnings (ims, hms) ws -> do
-- visible metas (goals)
goals <- mapM convertGoal ims
-- hidden (unsolved) metas
metas <- mapM convertHiddenMeta hms
-- errors / warnings
-- filter
#if MIN_VERSION_Agda(2,8,0)
filteredWarnings <- filterTCWarnings (tcWarnings ws)
filteredErrors <- filterTCWarnings (nonFatalErrors ws)
#else
let filteredWarnings = filterTCWarnings (tcWarnings ws)
let filteredErrors = filterTCWarnings (nonFatalErrors ws)
#endif
-- serializes
warnings <- mapM prettyTCM filteredWarnings
errors <- mapM prettyTCM filteredErrors
let isG = not (null goals && null metas)
let isW = not $ null warnings
let isE = not $ null errors
let title =
List.intercalate "," $
catMaybes
[ " Goals" <$ guard isG,
" Errors" <$ guard isE,
" Warnings" <$ guard isW,
" Done" <$ guard (not (isG || isW || isE))
]
return $ IR.DisplayInfoAllGoalsWarnings ("*All" ++ title ++ "*") goals metas (fmap show warnings) (fmap show errors)
where
convertHiddenMeta :: OutputConstraint A.Expr NamedMeta -> TCM Block
convertHiddenMeta m = do
let i = nmid $ namedMetaOf m
-- output constrain
meta <- withMetaId i $ renderATop m
serialized <- show <$> withMetaId i (prettyATop m)
-- range
range <- getMetaRange i
return $ Unlabeled meta (Just serialized) (Just range)
convertGoal :: OutputConstraint A.Expr InteractionId -> TCM Block
convertGoal i = do
-- output constrain
goal <-
withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock i) $
renderATop i
serialized <-
withInteractionId (outputFormId $ OutputForm noRange [] alwaysUnblock i) $
prettyATop i
return $ Unlabeled goal (Just $ show serialized) Nothing
Info_Auto s -> return $ IR.DisplayInfoAuto s
Info_Error err -> do
s <- showInfoError err
return $ IR.DisplayInfoError s
Info_Time s ->
return $ IR.DisplayInfoTime (show (prettyTimed s))
Info_NormalForm state cmode time expr -> do
exprDoc <- evalStateT prettyExpr state
let doc = maybe empty prettyTimed time $$ exprDoc
return $ IR.DisplayInfoNormalForm (show doc)
where
prettyExpr =
localStateCommandM $
lift $
B.atTopLevel $
allowNonTerminatingReductions $
(if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode) $
B.showComputed cmode expr
Info_InferredType state time expr -> do
renderedExpr <-
flip evalStateT state $
localStateCommandM $
lift $
B.atTopLevel $
Render.renderA expr
let rendered = case time of
Nothing -> renderedExpr
-- TODO: handle this newline
Just t -> "Time:" Render.<+> Render.render t Render.<+> "\n" Render.<+> renderedExpr
exprDoc <-
flip evalStateT state $
localStateCommandM $
lift $
B.atTopLevel $
TCP.prettyA expr
let raw = show $ maybe empty prettyTimed time $$ exprDoc
return $ IR.DisplayInfoGeneric "Inferred Type" [Unlabeled rendered (Just raw) Nothing]
Info_ModuleContents modules tel types -> do
doc <- localTCState $ do
typeDocs <- addContext tel $
forM types $ \(x, t) -> do
doc <- prettyTCM t
return (prettyShow x, ":" <+> doc)
return $
vcat
[ "Modules",
nest 2 $ vcat $ fmap pretty modules,
"Names",
nest 2 $ align 10 typeDocs
]
return $ IR.DisplayInfoGeneric "Module contents" [Unlabeled (Render.text $ show doc) Nothing Nothing]
Info_SearchAbout hits names -> do
hitDocs <- forM hits $ \(x, t) -> do
doc <- prettyTCM t
return (prettyShow x, ":" <+> doc)
let doc =
"Definitions about"
<+> text (List.intercalate ", " $ words names)
$$ nest 2 (align 10 hitDocs)
return $ IR.DisplayInfoGeneric "Search About" [Unlabeled (Render.text $ show doc) Nothing Nothing]
Info_WhyInScope why -> do
doc <- explainWhyInScope why
return $ IR.DisplayInfoGeneric "Scope Info" [Unlabeled (Render.text $ show doc) Nothing Nothing]
Info_Context ii ctx -> do
doc <- localTCState (prettyResponseContexts ii False ctx)
return $ IR.DisplayInfoGeneric "Context" [Unlabeled (Render.text $ show doc) Nothing Nothing]
Info_Intro_NotFound ->
return $ IR.DisplayInfoGeneric "Intro" [Unlabeled (Render.text "No introduction forms found.") Nothing Nothing]
Info_Intro_ConstructorUnknown ss -> do
let doc =
sep
[ "Don't know which constructor to introduce of",
let mkOr [] = []
mkOr [x, y] = [text x <+> "or" <+> text y]
mkOr (x : xs) = text x : mkOr xs
in nest 2 $ fsep $ punctuate comma (mkOr ss)
]
return $ IR.DisplayInfoGeneric "Intro" [Unlabeled (Render.text $ show doc) Nothing Nothing]
Info_Version ->
return $ IR.DisplayInfoGeneric "Agda Version" [Unlabeled (Render.text $ "Agda version " ++ versionWithCommitInfo) Nothing Nothing]
Info_GoalSpecific ii kind -> lispifyGoalSpecificDisplayInfo ii kind
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM IR.DisplayInfo
lispifyGoalSpecificDisplayInfo ii kind = localTCState $
withInteractionId ii $
case kind of
Goal_HelperFunction helperType -> do
doc <- inTopContext $ prettyATop helperType
return $ IR.DisplayInfoGeneric "Helper function" [Unlabeled (Render.text $ show doc ++ "\n") Nothing Nothing]
Goal_NormalForm cmode expr -> do
doc <- showComputed cmode expr
return $ IR.DisplayInfoGeneric "Normal Form" [Unlabeled (Render.text $ show doc) Nothing Nothing]
Goal_GoalType norm aux resCtxs boundaries constraints -> do
goalSect <- do
(rendered, raw) <- prettyTypeOfMeta norm ii
return [Labeled rendered (Just raw) Nothing "Goal" "special"]
auxSect <- case aux of
GoalOnly -> return []
GoalAndHave expr bndry -> do
-- TODO: render bndry
rendered <- renderATop expr
raw <- show <$> prettyATop expr
return [Labeled rendered (Just raw) Nothing "Have" "special"]
GoalAndElaboration expr -> do
#if MIN_VERSION_Agda(2,8,0)
rendered <- renderATop expr
#else
let rendered = render expr
#endif
raw <- show <$> TCP.prettyTCM expr
return [Labeled rendered (Just raw) Nothing "Elaborates to" "special"]
let boundarySect =
if null boundaries
then []
else
Header "Boundary"
: fmap (\boundary -> Unlabeled (render boundary) (Just $ show $ pretty boundary) Nothing) boundaries
contextSect <- reverse . concat <$> mapM (renderResponseContext ii) resCtxs
let constraintSect =
if null constraints
then []
else
Header "Constraints"
: fmap (\constraint -> Unlabeled (render constraint) (Just $ show $ pretty constraint) Nothing) constraints
return $
IR.DisplayInfoGeneric "Goal type etc" $
goalSect ++ auxSect ++ boundarySect ++ contextSect ++ constraintSect
Goal_CurrentGoal norm -> do
(rendered, raw) <- prettyTypeOfMeta norm ii
return $ IR.DisplayInfoCurrentGoal (Unlabeled rendered (Just raw) Nothing)
Goal_InferredType expr -> do
rendered <- renderATop expr
raw <- show <$> prettyATop expr
return $ IR.DisplayInfoInferredType (Unlabeled rendered (Just raw) Nothing)
-- -- | Format responses of DisplayInfo
-- formatPrim :: Bool -> [Block] -> String -> TCM IR.DisplayInfo
-- formatPrim _copy items header = return $ IR.DisplayInfoGeneric header items
-- -- | Format responses of DisplayInfo ("agda2-info-action")
-- format :: [Block] -> String -> TCM IR.DisplayInfo
-- format = formatPrim False
-- -- | Format responses of DisplayInfo ("agda2-info-action-copy")
-- formatAndCopy :: [Block] -> String -> TCM IR.DisplayInfo
-- formatAndCopy = formatPrim True
--------------------------------------------------------------------------------
-- | Pretty-prints the context of the given meta-variable.
prettyResponseContexts ::
-- | Context of this meta-variable.
InteractionId ->
-- | Print the elements in reverse order?
Bool ->
[ResponseContextEntry] ->
TCM Doc
prettyResponseContexts ii rev ctxs = do
rows <- mapM (prettyResponseContext ii) ctxs
return $ align 10 $ concat $ applyWhen rev reverse rows
-- | Pretty-prints the context of the given meta-variable.
prettyResponseContext ::
-- | Context of this meta-variable.
InteractionId ->
ResponseContextEntry ->
TCM [(String, Doc)]
prettyResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
modality <- currentModality
do
let prettyCtxName :: String
prettyCtxName
| n == x = prettyShow x
| isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
| otherwise = prettyShow x
-- Some attributes are useful to report whenever they are not
-- in the default state.
attribute :: String
attribute = c ++ if null c then "" else " "
where
c = prettyShow (getCohesion ai)
extras :: [Doc]
extras =
concat
[ ["not in scope" | isInScope nis == C.NotInScope],
-- Print erased if hypothesis is erased by goal is non-erased.
["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
-- Print irrelevant if hypothesis is strictly less relevant than goal.
["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
-- Print instance if variable is considered by instance search
["instance" | isInstance ai]
]
ty <- prettyATop expr
letv' <- case letv of
Nothing -> return []
Just val -> do
val' <- prettyATop val
return [(prettyShow x, "=" <+> val')]
return $
(attribute ++ prettyCtxName, ":" <+> ty <+> parenSep extras) : letv'
where
parenSep :: [Doc] -> Doc
parenSep docs
| null docs = empty
| otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs
-- | Render the context of the given meta-variable.
renderResponseContext ::
-- | Context of this meta-variable.
InteractionId ->
ResponseContextEntry ->
TCM [Block]
renderResponseContext ii (ResponseContextEntry n x (Arg ai expr) letv nis) = withInteractionId ii $ do
modality <- currentModality
do
let rawCtxName :: String
rawCtxName
| n == x = prettyShow x
| isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x
| otherwise = prettyShow x
renderedCtxName :: Inlines
renderedCtxName
| n == x = render x
| isInScope n == InScope = render n Render.<+> "=" Render.<+> render x
| otherwise = render x
-- Some attributes are useful to report whenever they are not
-- in the default state.
rawAttribute :: String
rawAttribute = c ++ if null c then "" else " "
where
c = prettyShow (getCohesion ai)
renderedAttribute :: Inlines
renderedAttribute = c <> if null (show c) then "" else " "
where
c = render (getCohesion ai)
extras :: (IsString a) => [a]
extras =
concat
[ ["not in scope" | isInScope nis == C.NotInScope],
-- Print erased if hypothesis is erased by goal is non-erased.
["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
-- Print irrelevant if hypothesis is strictly less relevant than goal.
["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
-- Print instance if variable is considered by instance search
["instance" | isInstance ai]
]
extras2 :: [Inlines]
extras2 =
concat
[ ["not in scope" | isInScope nis == C.NotInScope],
-- Print erased if hypothesis is erased by goal is non-erased.
["erased" | not $ getQuantity ai `moreQuantity` getQuantity modality],
-- Print irrelevant if hypothesis is strictly less relevant than goal.
["irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance modality],
-- Print instance if variable is considered by instance search
["instance" | isInstance ai]
]
-- raw
rawExpr <- prettyATop expr
let rawType = show $ align 10 [(rawAttribute ++ rawCtxName, ":" <+> rawExpr <+> parenSep extras)]
-- rendered
renderedExpr <- renderATop expr
let renderedType = (renderedCtxName <> renderedAttribute) Render.<+> ":" Render.<+> renderedExpr Render.<+> parenSep2 extras2
-- (Render.fsep $ Render.punctuate "," extras)
-- result
let typeItem = Unlabeled renderedType (Just rawType) Nothing
valueItem <- case letv of
Nothing -> return []
Just val -> do
valText <- renderATop val
valString <- prettyATop val
let renderedValue = Render.render x Render.<+> "=" Render.<+> valText
let rawValue = show $ align 10 [(prettyShow x, "=" <+> valString)]
return
[ Unlabeled renderedValue (Just rawValue) Nothing
]
return $ typeItem : valueItem
where
parenSep :: [Doc] -> Doc
parenSep docs
| null docs = empty
| otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs
parenSep2 :: [Inlines] -> Inlines
parenSep2 docs
| null docs = mempty
| otherwise = (" " Render.<+>) $ Render.parens $ Render.fsep $ Render.punctuate "," docs
-- | Pretty-prints the type of the meta-variable.
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
prettyTypeOfMeta norm ii = do
form <- B.typeOfMeta norm ii
case form of
OfType _ e -> do
rendered <- renderATop e
raw <- show <$> prettyATop e
return (rendered, raw)
_ -> do
rendered <- renderATop form
raw <- show <$> prettyATop form
return (rendered, raw)
-- | Prefix prettified CPUTime with "Time:"
prettyTimed :: CPUTime -> Doc
prettyTimed time = "Time:" <+> pretty time