{-# LANGUAGE OverloadedStrings #-} module Cornelis.Pretty where import Cornelis.Offsets (AgdaPos, Pos(..), Interval(..), AgdaInterval, charToBytes, textToBytes) import qualified Cornelis.Types as C import qualified Cornelis.Types as X import Cornelis.Types hiding (Type) import Data.Bool (bool) import Data.Function (on) import Data.Int import Data.List (sortOn, groupBy, intersperse) import qualified Data.Map as M import Data.Maybe (maybeToList, fromMaybe, fromJust) import Data.Semigroup (stimes) import qualified Data.Text as T import Prettyprinter import Prettyprinter.Internal.Type -- | Custom highlight groups set by the plugin. -- -- These groups linked to Neovim default highlight groups in @syntax/agda.vim@. -- -- The suffix after @Cornelis/XXX/@ matches the names as returned by Agda, contained in 'C.hl_atoms'. -- How these names are generated is not documented on Agda's side, but the implementation can be found at -- ['Agda.Interaction.Highlighting.Common.toAtoms'](https://github.com/agda/agda/src/full/Agda/Interaction/Highlighting/Common.hs). -- The correspoding Agda types are found in 'Agda.Interaction.Highlighting.Precise'. -- -- NOTE: -- * When modifying this type, remember to sync the changes to @syntax/agda.vim@ -- * This list of highlight groups does not yet cover all variants returned by Agda data HighlightGroup = CornelisError -- ^ InfoWin highlight group of error messages | CornelisErrorWarning -- ^ InfoWin highlight group of warnings considered fatal | CornelisWarn -- ^ InfoWin highlight group of warnings | CornelisTitle -- ^ InfoWin highlight of section titles | CornelisName -- ^ InfoWin highlight of names in context | CornelisHole -- ^ An open hole (@{! /.../ !}@ and @?@) | CornelisUnsolvedMeta -- ^ An unresolved meta variable | CornelisUnsolvedConstraint -- ^ An unresolved constraint | CornelisKeyword -- ^ An Agda keywords (@where@, @let@, etc.) | CornelisSymbol -- ^ A symbol, not part of an identifier (@=@, @:@, @{@, etc.) | CornelisType -- ^ A datatype (@Nat@, @Bool@, etc.) | CornelisPrimitiveType -- ^ A primitive/builtin Agda type | CornelisRecord -- ^ A datatype, defined as a @record@ | CornelisFunction -- ^ A function, e.g. a top-level declaration | CornelisArgument -- ^ The name of an (implicit) argument, i.e. @Foo {/bar/ = 42}@ | CornelisBound -- ^ A bound identifier, e.g. a variable in a pattern clause or a module parameter | CornelisOperator -- ^ A mixfix operator, e.g. @x /∷/ xs@. | CornelisField -- ^ Field of a record definition | CornelisGeneralizable -- ^ A generalizable variable, defined for example in a @variable@ block | CornelisMacro -- ^ A macro, defined in a @macro@ block | CornelisInductiveConstructor -- ^ A constructor of an inductive data type (e.g. @data Foo /.../@) | CornelisCoinductiveConstructor -- ^ A constructor for a /co/inductive datatype, i.e. a record marked @coinductive@ | CornelisNumber -- ^ A number literal | CornelisComment -- ^ A comment | CornelisString -- ^ A string literal | CornelisCatchAllClause -- ^ "Catch-all clause". Some sort of fallback; not exactly clear where this is used | CornelisTypeChecks -- ^ A location being type-checked right now | CornelisModule -- ^ A module name, e.g. in a @module@ block or an @import@ | CornelisPostulate -- ^ A term, defined in a @postulate@ block | CornelisPrimitive -- ^ An Agda primitive, e.g. @Set@ | CornelisPragma -- ^ The argument to a pragma, e.g. @{-# OPTIONS /--foo/ -#}@ deriving (Eq, Ord, Show, Read, Enum, Bounded) -- | Priority of the HighlightGroup. See `:h vim.highlight.priorities` for more information. -- -- 100 is the default syntax highlighting priority, while 150 is reserved for diagnostics. priority :: HighlightGroup -> Int64 priority CornelisError = 150 priority CornelisErrorWarning = 150 priority CornelisWarn = 150 priority CornelisUnsolvedMeta = 150 priority CornelisUnsolvedConstraint = 150 priority _ = 100 atomToHlGroup :: Text -> Maybe HighlightGroup atomToHlGroup atom = M.lookup atom allHlGroups where stripCornelis = fromJust . T.stripPrefix "Cornelis" toAtomName :: HighlightGroup -> Text toAtomName hlGroup = T.toLower $ stripCornelis $ T.pack $ show hlGroup allHlGroups :: M.Map Text HighlightGroup allHlGroups = M.fromList $ map (\g -> (toAtomName g, g)) [(minBound :: HighlightGroup) ..] data InfoHighlight a = InfoHighlight { ihl_start :: (Int64, Int64) , ihl_end :: a , ihl_group :: HighlightGroup } deriving (Eq, Ord, Show, Functor) spanInfoHighlights :: InfoHighlight (Int64, Int64) -> [InfoHighlight Int64] spanInfoHighlights ih@(InfoHighlight (sl, sc) (el, ec) hg) | sl == el = pure $ fmap snd ih | otherwise = InfoHighlight (sl, sc) (-1) hg : InfoHighlight (el, 0) ec hg : fmap (\l -> InfoHighlight (l, 0) (-1) hg) [sl + 1 .. el - 1] renderWithHlGroups :: SimpleDocStream HighlightGroup -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a) renderWithHlGroups = go [] 0 0 where go :: [InfoHighlight ()] -> Int64 -> Int64 -> SimpleDocStream HighlightGroup -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a) go _ _ _ SFail = pure SFail go _ _ _ SEmpty = pure SEmpty go st r c (SChar c' sds) = SChar c' <$> go st r (c + fromIntegral (charToBytes c')) sds go st r c (SText n txt sds) = SText n txt <$> go st r (c + fromIntegral (textToBytes txt)) sds go st r _ (SLine n sds) = SLine n <$> go st (r + 1) (fromIntegral n) sds go st r c (SAnnPush hg sds) = go (InfoHighlight (r, c) () hg : st) r c sds go [] _ _ (SAnnPop _) = error "popping an annotation that doesn't exist" go (ih : ihs) r c (SAnnPop sds) = do sds' <- go ihs r c sds ([(r, c) <$ ih], sds') prettyType :: C.Type -> Doc HighlightGroup prettyType (C.Type ty) = annotate CornelisType $ sep $ fmap pretty $ T.lines ty groupScopeSet :: [InScope] -> [[InScope]] groupScopeSet = sortOn (is_refied_name . head) . fmap (sortOn is_refied_name) . groupBy (on (==) is_type) . sortOn is_type prettyGoals :: DisplayInfo -> Doc HighlightGroup prettyGoals (AllGoalsWarnings vis invis errs warns) = vcat $ punctuate hardline $ filter (not . isEmpty) [ section "Warnings" warns $ annotate CornelisWarn . pretty . getMessage , section "Visible Goals" vis $ prettyGoal . fmap (mappend "?" . T.pack . show . ip_id) , section "Errors" errs prettyError , section "Invisible Goals" invis $ \gi -> prettyGoal (fmap np_name gi) <+> maybe mempty (brackets . ("at" <+>) . prettyInterval) (np_interval $ gi_ip gi) ] prettyGoals (GoalSpecific _ scoped ty mhave mboundary mconstraints) = vcat $ intersperse (stimes @_ @Int 60 "—") $ [ section "Boundary" (fromMaybe [] mboundary) pretty ] <> [ annotate CornelisTitle "Goal:" <+> prettyType ty ] <> [ annotate CornelisTitle "Have:" <+> prettyType have | have <- maybeToList mhave ] <> [ vcat $ fmap prettyInScopeSet $ groupScopeSet scoped ] <> [ section "Constraints" (fromMaybe [] mconstraints) pretty ] prettyGoals (HelperFunction sig) = section "Helper Function" [ mempty , annotate CornelisType $ pretty sig , mempty , annotate CornelisComment $ parens "copied to \" register" ] id prettyGoals (InferredType ty) = annotate CornelisTitle "Inferred Type:" <+> prettyType ty prettyGoals (WhyInScope msg) = pretty msg prettyGoals (NormalForm expr) = pretty expr prettyGoals (DisplayError err) = annotate CornelisError $ pretty err prettyGoals (UnknownDisplayInfo v) = annotate CornelisError $ pretty $ show v prettyInterval :: AgdaInterval -> Doc HighlightGroup prettyInterval (Interval s e) | p_line s == p_line e = prettyPoint s <> "-" <> pretty (p_col e) | otherwise = prettyPoint s <> "-" <> prettyPoint e prettyPoint :: AgdaPos -> Doc HighlightGroup prettyPoint p = pretty (p_line p) <> "," <> pretty (p_col p) isEmpty :: Doc HighlightGroup -> Bool isEmpty Empty = True isEmpty _ = False section :: Doc HighlightGroup -> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup section _ [] _ = mempty section doc as f = vcat $ annotate CornelisTitle (doc <> ":") : fmap f as prettyName :: Text -> Doc HighlightGroup prettyName = prettyVisibleName True prettyVisibleName :: Bool -> Text -> Doc HighlightGroup prettyVisibleName False t = annotate CornelisComment $ "(" <> pretty t <> ")" prettyVisibleName True t = annotate CornelisName $ pretty t prettyInScope :: InScope -> Doc HighlightGroup prettyInScope (InScope reified _ in_scope ty) = hsep [ prettyGoal $ GoalInfo reified ty , bool (pretty (replicate 6 ' ') <+> annotate CornelisComment (parens "not in scope")) mempty in_scope ] prettyInScopeSet :: [InScope] -> Doc HighlightGroup prettyInScopeSet is = let ty = is_type $ head is in prettyManyGoals is ty prettyManyGoals :: [InScope] -> X.Type -> Doc HighlightGroup prettyManyGoals is ty = hang 4 $ sep [ hsep $ fmap (\i -> prettyVisibleName (is_in_scope i) $ is_refied_name i) is <> [":"] , prettyType ty ] prettyGoal :: GoalInfo Text -> Doc HighlightGroup prettyGoal (GoalInfo name ty) = hang 4 $ sep [ prettyName name <+> ":" , prettyType ty ] prettyError :: Message -> Doc HighlightGroup prettyError (Message msg) = let (hdr, body) = fmap (T.drop 1) $ T.break (== '\n') msg in vcat [ annotate CornelisError (pretty hdr) , pretty body ]