1module Agda.Interaction.EmacsTop 2 ( mimicGHCi 3 , namedMetaOf 4 , showGoals 5 , showInfoError 6 , explainWhyInScope 7 , prettyTypeOfMeta 8 ) where 9 10import Control.Monad.State hiding (state) 11import qualified Data.List as List 12 13import Agda.Syntax.Common 14import Agda.Syntax.Position 15import Agda.Syntax.Scope.Base 16import Agda.Syntax.Abstract.Pretty (prettyATop) 17import Agda.Syntax.Abstract as A 18import Agda.Syntax.Concrete as C 19 20import Agda.TypeChecking.Errors (prettyError, getAllWarningsOfTCErr) 21import qualified Agda.TypeChecking.Pretty as TCP 22import Agda.TypeChecking.Pretty (prettyTCM) 23import Agda.TypeChecking.Pretty.Warning (prettyTCWarnings, prettyTCWarnings') 24import Agda.TypeChecking.Monad 25import Agda.TypeChecking.Warnings (WarningsAndNonFatalErrors(..)) 26import Agda.Interaction.AgdaTop 27import Agda.Interaction.Base 28import Agda.Interaction.BasicOps as B 29import Agda.Interaction.Response as R 30import Agda.Interaction.EmacsCommand hiding (putResponse) 31import Agda.Interaction.Highlighting.Emacs 32import Agda.Interaction.Highlighting.Precise (TokenBased(..)) 33import Agda.Interaction.InteractionTop (localStateCommandM) 34import Agda.Utils.Function (applyWhen) 35import Agda.Utils.Null (empty) 36import Agda.Utils.Maybe 37import Agda.Utils.Pretty 38import Agda.Utils.String 39import Agda.Utils.Time (CPUTime) 40import Agda.VersionCommit 41 42---------------------------------- 43 44-- | 'mimicGHCi' is a fake ghci interpreter for the Emacs frontend 45-- and for interaction tests. 46-- 47-- 'mimicGHCi' reads the Emacs frontend commands from stdin, 48-- interprets them and print the result into stdout. 49mimicGHCi :: TCM () -> TCM () 50mimicGHCi = repl (liftIO . mapM_ (putStrLn . prettyShow) <=< lispifyResponse) "Agda2> " 51 52-- | Convert Response to an elisp value for the interactive emacs frontend. 53 54lispifyResponse :: Response -> TCM [Lisp String] 55lispifyResponse (Resp_HighlightingInfo info remove method modFile) = 56 (:[]) <$> liftIO (lispifyHighlightingInfo info remove method modFile) 57lispifyResponse (Resp_DisplayInfo info) = lispifyDisplayInfo info 58lispifyResponse (Resp_ClearHighlighting tokenBased) = 59 return [ L $ A "agda2-highlight-clear" : 60 case tokenBased of 61 NotOnlyTokenBased -> [] 62 TokenBased -> 63 [ Q (lispifyTokenBased tokenBased) ] 64 ] 65lispifyResponse Resp_DoneAborting = return [ L [ A "agda2-abort-done" ] ] 66lispifyResponse Resp_DoneExiting = return [ L [ A "agda2-exit-done" ] ] 67lispifyResponse Resp_ClearRunningInfo = return [ clearRunningInfo ] 68lispifyResponse (Resp_RunningInfo n s) 69 | n <= 1 = return [ displayRunningInfo s ] 70 | otherwise = return [ L [A "agda2-verbose", A (quote s)] ] 71lispifyResponse (Resp_Status s) 72 = return [ L [ A "agda2-status-action" 73 , A (quote $ List.intercalate "," $ catMaybes [checked, showImpl, showIrr]) 74 ] 75 ] 76 where 77 checked = boolToMaybe (sChecked s) "Checked" 78 showImpl = boolToMaybe (sShowImplicitArguments s) "ShowImplicit" 79 showIrr = boolToMaybe (sShowIrrelevantArguments s) "ShowIrrelevant" 80 81lispifyResponse (Resp_JumpToError f p) = return 82 [ lastTag 3 $ 83 L [ A "agda2-maybe-goto", Q $ L [A (quote f), A ".", A (show p)] ] 84 ] 85lispifyResponse (Resp_InteractionPoints is) = return 86 [ lastTag 1 $ 87 L [A "agda2-goals-action", Q $ L $ map showNumIId is] 88 ] 89lispifyResponse (Resp_GiveAction ii s) 90 = return [ L [ A "agda2-give-action", showNumIId ii, A s' ] ] 91 where 92 s' = case s of 93 Give_String str -> quote str 94 Give_Paren -> "'paren" 95 Give_NoParen -> "'no-paren" 96lispifyResponse (Resp_MakeCase ii variant pcs) = return 97 [ lastTag 2 $ L [ A cmd, Q $ L $ map (A . quote) pcs ] ] 98 where 99 cmd = case variant of 100 R.Function -> "agda2-make-case-action" 101 R.ExtendedLambda -> "agda2-make-case-action-extendlam" 102lispifyResponse (Resp_SolveAll ps) = return 103 [ lastTag 2 $ 104 L [ A "agda2-solveAll-action", Q . L $ concatMap prn ps ] 105 ] 106 where 107 prn (ii,e)= [showNumIId ii, A $ quote $ prettyShow e] 108 109lispifyDisplayInfo :: DisplayInfo -> TCM [Lisp String] 110lispifyDisplayInfo info = case info of 111 Info_CompilationOk ws -> do 112 warnings <- prettyTCWarnings (tcWarnings ws) 113 errors <- prettyTCWarnings (nonFatalErrors ws) 114 -- abusing the goals field since we ignore the title 115 let (body, _) = formatWarningsAndErrors 116 "The module was successfully compiled.\n" 117 warnings 118 errors 119 format body "*Compilation result*" 120 Info_Constraints s -> format (show $ vcat $ map pretty s) "*Constraints*" 121 Info_AllGoalsWarnings ms ws -> do 122 goals <- showGoals ms 123 warnings <- prettyTCWarnings (tcWarnings ws) 124 errors <- prettyTCWarnings (nonFatalErrors ws) 125 let (body, title) = formatWarningsAndErrors goals warnings errors 126 format body ("*All" ++ title ++ "*") 127 Info_Auto s -> format s "*Auto*" 128 Info_Error err -> do 129 s <- showInfoError err 130 format s "*Error*" 131 Info_Time s -> format (render $ prettyTimed s) "*Time*" 132 Info_NormalForm state cmode time expr -> do 133 exprDoc <- evalStateT prettyExpr state 134 let doc = maybe empty prettyTimed time $$ exprDoc 135 lbl | cmode == HeadCompute = "*Head Normal Form*" 136 | otherwise = "*Normal Form*" 137 format (render doc) lbl 138 where 139 prettyExpr = localStateCommandM 140 $ lift 141 $ B.atTopLevel 142 $ allowNonTerminatingReductions 143 $ (if computeIgnoreAbstract cmode then ignoreAbstractMode else inConcreteMode) 144 $ (B.showComputed cmode) 145 $ expr 146 Info_InferredType state time expr -> do 147 exprDoc <- evalStateT prettyExpr state 148 let doc = maybe empty prettyTimed time $$ exprDoc 149 format (render doc) "*Inferred Type*" 150 where 151 prettyExpr = localStateCommandM 152 $ lift 153 $ B.atTopLevel 154 $ TCP.prettyA 155 $ expr 156 Info_ModuleContents modules tel types -> do 157 doc <- localTCState $ do 158 typeDocs <- addContext tel $ forM types $ \ (x, t) -> do 159 doc <- prettyTCM t 160 return (prettyShow x, ":" <+> doc) 161 return $ vcat 162 [ "Modules" 163 , nest 2 $ vcat $ map pretty modules 164 , "Names" 165 , nest 2 $ align 10 typeDocs 166 ] 167 format (render doc) "*Module contents*" 168 Info_SearchAbout hits names -> do 169 hitDocs <- forM hits $ \ (x, t) -> do 170 doc <- prettyTCM t 171 return (prettyShow x, ":" <+> doc) 172 let doc = "Definitions about" <+> 173 text (List.intercalate ", " $ words names) $$ nest 2 (align 10 hitDocs) 174 format (render doc) "*Search About*" 175 Info_WhyInScope s cwd v xs ms -> do 176 doc <- explainWhyInScope s cwd v xs ms 177 format (render doc) "*Scope Info*" 178 Info_Context ii ctx -> do 179 doc <- localTCState (prettyResponseContext ii False ctx) 180 format (render doc) "*Context*" 181 Info_Intro_NotFound -> format "No introduction forms found." "*Intro*" 182 Info_Intro_ConstructorUnknown ss -> do 183 let doc = sep [ "Don't know which constructor to introduce of" 184 , let mkOr [] = [] 185 mkOr [x, y] = [text x <+> "or" <+> text y] 186 mkOr (x:xs) = text x : mkOr xs 187 in nest 2 $ fsep $ punctuate comma (mkOr ss) 188 ] 189 format (render doc) "*Intro*" 190 Info_Version -> format ("Agda version " ++ versionWithCommitInfo) "*Agda Version*" 191 Info_GoalSpecific ii kind -> lispifyGoalSpecificDisplayInfo ii kind 192 193lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM [Lisp String] 194lispifyGoalSpecificDisplayInfo ii kind = localTCState $ B.withInteractionId ii $ 195 case kind of 196 Goal_HelperFunction helperType -> do 197 doc <- inTopContext $ prettyATop helperType 198 return [ L [ A "agda2-info-action-and-copy" 199 , A $ quote "*Helper function*" 200 , A $ quote (render doc ++ "\n") 201 , A "nil" 202 ] 203 ] 204 Goal_NormalForm cmode expr -> do 205 doc <- showComputed cmode expr 206 format (render doc) "*Normal Form*" -- show? 207 Goal_GoalType norm aux ctx bndry constraints -> do 208 ctxDoc <- prettyResponseContext ii True ctx 209 goalDoc <- prettyTypeOfMeta norm ii 210 auxDoc <- case aux of 211 GoalOnly -> return empty 212 GoalAndHave expr -> do 213 doc <- prettyATop expr 214 return $ "Have:" <+> doc 215 GoalAndElaboration term -> do 216 doc <- TCP.prettyTCM term 217 return $ "Elaborates to:" <+> doc 218 let boundaryDoc 219 | null bndry = [] 220 | otherwise = [ text $ delimiter "Boundary" 221 , vcat $ map pretty bndry 222 ] 223 let constraintsDoc = if (null constraints) 224 then [] 225 else [ text $ delimiter "Constraints" 226 , vcat $ map pretty constraints 227 ] 228 let doc = vcat $ 229 [ "Goal:" <+> goalDoc 230 , auxDoc 231 , vcat boundaryDoc 232 , text (replicate 60 '\x2014') 233 , ctxDoc 234 ] ++ constraintsDoc 235 format (render doc) "*Goal type etc.*" 236 Goal_CurrentGoal norm -> do 237 doc <- prettyTypeOfMeta norm ii 238 format (render doc) "*Current Goal*" 239 Goal_InferredType expr -> do 240 doc <- prettyATop expr 241 format (render doc) "*Inferred Type*" 242 243-- | Format responses of DisplayInfo 244 245format :: String -> String -> TCM [Lisp String] 246format content bufname = return [ display_info' False bufname content ] 247 248-- | Adds a \"last\" tag to a response. 249 250lastTag :: Integer -> Lisp String -> Lisp String 251lastTag n r = Cons (Cons (A "last") (A $ show n)) r 252 253-- | Show an iteraction point identifier as an elisp expression. 254 255showNumIId :: InteractionId -> Lisp String 256showNumIId = A . show . interactionId 257 258-------------------------------------------------------------------------------- 259 260-- | Given strings of goals, warnings and errors, return a pair of the 261-- body and the title for the info buffer 262formatWarningsAndErrors :: String -> String -> String -> (String, String) 263formatWarningsAndErrors g w e = (body, title) 264 where 265 isG = not $ null g 266 isW = not $ null w 267 isE = not $ null e 268 title = List.intercalate "," $ catMaybes 269 [ " Goals" <$ guard isG 270 , " Errors" <$ guard isE 271 , " Warnings" <$ guard isW 272 , " Done" <$ guard (not (isG || isW || isE)) 273 ] 274 275 body = List.intercalate "\n" $ catMaybes 276 [ g <$ guard isG 277 , delimiter "Errors" <$ guard (isE && (isG || isW)) 278 , e <$ guard isE 279 , delimiter "Warnings" <$ guard (isW && (isG || isE)) 280 , w <$ guard isW 281 ] 282 283 284-- | Serializing Info_Error 285showInfoError :: Info_Error -> TCM String 286showInfoError (Info_GenericError err) = do 287 e <- prettyError err 288 w <- prettyTCWarnings' =<< getAllWarningsOfTCErr err 289 290 let errorMsg = if null w 291 then e 292 else delimiter "Error" ++ "\n" ++ e 293 let warningMsg = List.intercalate "\n" $ delimiter "Warning(s)" 294 : filter (not . null) w 295 return $ if null w 296 then errorMsg 297 else errorMsg ++ "\n\n" ++ warningMsg 298showInfoError (Info_CompilationError warnings) = do 299 s <- prettyTCWarnings warnings 300 return $ unlines 301 [ "You need to fix the following errors before you can compile" 302 , "the module:" 303 , "" 304 , s 305 ] 306showInfoError (Info_HighlightingParseError ii) = 307 return $ "Highlighting failed to parse expression in " ++ show ii 308showInfoError (Info_HighlightingScopeCheckError ii) = 309 return $ "Highlighting failed to scope check expression in " ++ show ii 310 311explainWhyInScope :: FilePath 312 -> String 313 -> (Maybe LocalVar) 314 -> [AbstractName] 315 -> [AbstractModule] 316 -> TCM Doc 317explainWhyInScope s _ Nothing [] [] = TCP.text (s ++ " is not in scope.") 318explainWhyInScope s _ v xs ms = TCP.vcat 319 [ TCP.text (s ++ " is in scope as") 320 , TCP.nest 2 $ TCP.vcat [variable v xs, modules ms] 321 ] 322 where 323 -- variable :: Maybe _ -> [_] -> TCM Doc 324 variable Nothing vs = names vs 325 variable (Just x) vs 326 | null vs = asVar 327 | otherwise = TCP.vcat 328 [ TCP.sep [ asVar, TCP.nest 2 $ shadowing x] 329 , TCP.nest 2 $ names vs 330 ] 331 where 332 asVar :: TCM Doc 333 asVar = do 334 "* a variable bound at" TCP.<+> TCP.prettyTCM (nameBindingSite $ localVar x) 335 shadowing :: LocalVar -> TCM Doc 336 shadowing (LocalVar _ _ []) = "shadowing" 337 shadowing _ = "in conflict with" 338 names = TCP.vcat . map pName 339 modules = TCP.vcat . map pMod 340 341 pKind = \case 342 ConName -> "constructor" 343 CoConName -> "coinductive constructor" 344 FldName -> "record field" 345 PatternSynName -> "pattern synonym" 346 GeneralizeName -> "generalizable variable" 347 DisallowedGeneralizeName -> "generalizable variable from let open" 348 MacroName -> "macro name" 349 QuotableName -> "quotable name" 350 -- previously DefName: 351 DataName -> "data type" 352 RecName -> "record type" 353 AxiomName -> "postulate" 354 PrimName -> "primitive function" 355 FunName -> "defined name" 356 OtherDefName -> "defined name" 357 358 pName :: AbstractName -> TCM Doc 359 pName a = TCP.sep 360 [ "* a" 361 TCP.<+> pKind (anameKind a) 362 TCP.<+> TCP.text (prettyShow $ anameName a) 363 , TCP.nest 2 $ "brought into scope by" 364 ] TCP.$$ 365 TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ anameName a) (anameLineage a)) 366 pMod :: AbstractModule -> TCM Doc 367 pMod a = TCP.sep 368 [ "* a module" TCP.<+> TCP.text (prettyShow $ amodName a) 369 , TCP.nest 2 $ "brought into scope by" 370 ] TCP.$$ 371 TCP.nest 2 (pWhy (nameBindingSite $ qnameName $ mnameToQName $ amodName a) (amodLineage a)) 372 373 pWhy :: Range -> WhyInScope -> TCM Doc 374 pWhy r Defined = "- its definition at" TCP.<+> TCP.prettyTCM r 375 pWhy r (Opened (C.QName x) w) | isNoName x = pWhy r w 376 pWhy r (Opened m w) = 377 "- the opening of" 378 TCP.<+> TCP.prettyTCM m 379 TCP.<+> "at" 380 TCP.<+> TCP.prettyTCM (getRange m) 381 TCP.$$ 382 pWhy r w 383 pWhy r (Applied m w) = 384 "- the application of" 385 TCP.<+> TCP.prettyTCM m 386 TCP.<+> "at" 387 TCP.<+> TCP.prettyTCM (getRange m) 388 TCP.$$ 389 pWhy r w 390 391 392-- | Pretty-prints the context of the given meta-variable. 393 394prettyResponseContext 395 :: InteractionId -- ^ Context of this meta-variable. 396 -> Bool -- ^ Print the elements in reverse order? 397 -> [ResponseContextEntry] 398 -> TCM Doc 399prettyResponseContext ii rev ctx = withInteractionId ii $ do 400 mod <- asksTC getModality 401 align 10 . concat . applyWhen rev reverse <$> do 402 forM ctx $ \ (ResponseContextEntry n x (Arg ai expr) letv nis) -> do 403 let 404 prettyCtxName :: String 405 prettyCtxName 406 | n == x = prettyShow x 407 | isInScope n == InScope = prettyShow n ++ " = " ++ prettyShow x 408 | otherwise = prettyShow x 409 410 -- Some attributes are useful to report whenever they are not 411 -- in the default state. 412 attribute :: String 413 attribute = c ++ if null c then "" else " " 414 where c = prettyShow (getCohesion ai) 415 416 extras :: [Doc] 417 extras = concat $ 418 [ [ "not in scope" | isInScope nis == C.NotInScope ] 419 -- Print erased if hypothesis is erased by goal is non-erased. 420 , [ "erased" | not $ getQuantity ai `moreQuantity` getQuantity mod ] 421 -- Print irrelevant if hypothesis is strictly less relevant than goal. 422 , [ "irrelevant" | not $ getRelevance ai `moreRelevant` getRelevance mod ] 423 -- Print instance if variable is considered by instance search 424 , [ "instance" | isInstance ai ] 425 ] 426 ty <- prettyATop expr 427 maybeVal <- traverse prettyATop letv 428 429 return $ 430 (attribute ++ prettyCtxName, ":" <+> ty <+> (parenSep extras)) : 431 [ (prettyShow x, "=" <+> val) | val <- maybeToList maybeVal ] 432 433 where 434 parenSep :: [Doc] -> Doc 435 parenSep docs 436 | null docs = empty 437 | otherwise = (" " <+>) $ parens $ fsep $ punctuate comma docs 438 439 440-- | Pretty-prints the type of the meta-variable. 441 442prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM Doc 443prettyTypeOfMeta norm ii = do 444 form <- B.typeOfMeta norm ii 445 case form of 446 OfType _ e -> prettyATop e 447 _ -> prettyATop form 448 449-- | Prefix prettified CPUTime with "Time:" 450prettyTimed :: CPUTime -> Doc 451prettyTimed time = "Time:" <+> pretty time 452