{-# 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 (HighlightGroup -> HighlightGroup -> Bool
(HighlightGroup -> HighlightGroup -> Bool)
-> (HighlightGroup -> HighlightGroup -> Bool) -> Eq HighlightGroup
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HighlightGroup -> HighlightGroup -> Bool
== :: HighlightGroup -> HighlightGroup -> Bool
$c/= :: HighlightGroup -> HighlightGroup -> Bool
/= :: HighlightGroup -> HighlightGroup -> Bool
Eq, Eq HighlightGroup
Eq HighlightGroup =>
(HighlightGroup -> HighlightGroup -> Ordering)
-> (HighlightGroup -> HighlightGroup -> Bool)
-> (HighlightGroup -> HighlightGroup -> Bool)
-> (HighlightGroup -> HighlightGroup -> Bool)
-> (HighlightGroup -> HighlightGroup -> Bool)
-> (HighlightGroup -> HighlightGroup -> HighlightGroup)
-> (HighlightGroup -> HighlightGroup -> HighlightGroup)
-> Ord HighlightGroup
HighlightGroup -> HighlightGroup -> Bool
HighlightGroup -> HighlightGroup -> Ordering
HighlightGroup -> HighlightGroup -> HighlightGroup
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: HighlightGroup -> HighlightGroup -> Ordering
compare :: HighlightGroup -> HighlightGroup -> Ordering
$c< :: HighlightGroup -> HighlightGroup -> Bool
< :: HighlightGroup -> HighlightGroup -> Bool
$c<= :: HighlightGroup -> HighlightGroup -> Bool
<= :: HighlightGroup -> HighlightGroup -> Bool
$c> :: HighlightGroup -> HighlightGroup -> Bool
> :: HighlightGroup -> HighlightGroup -> Bool
$c>= :: HighlightGroup -> HighlightGroup -> Bool
>= :: HighlightGroup -> HighlightGroup -> Bool
$cmax :: HighlightGroup -> HighlightGroup -> HighlightGroup
max :: HighlightGroup -> HighlightGroup -> HighlightGroup
$cmin :: HighlightGroup -> HighlightGroup -> HighlightGroup
min :: HighlightGroup -> HighlightGroup -> HighlightGroup
Ord, Int -> HighlightGroup -> ShowS
[HighlightGroup] -> ShowS
HighlightGroup -> String
(Int -> HighlightGroup -> ShowS)
-> (HighlightGroup -> String)
-> ([HighlightGroup] -> ShowS)
-> Show HighlightGroup
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HighlightGroup -> ShowS
showsPrec :: Int -> HighlightGroup -> ShowS
$cshow :: HighlightGroup -> String
show :: HighlightGroup -> String
$cshowList :: [HighlightGroup] -> ShowS
showList :: [HighlightGroup] -> ShowS
Show, ReadPrec [HighlightGroup]
ReadPrec HighlightGroup
Int -> ReadS HighlightGroup
ReadS [HighlightGroup]
(Int -> ReadS HighlightGroup)
-> ReadS [HighlightGroup]
-> ReadPrec HighlightGroup
-> ReadPrec [HighlightGroup]
-> Read HighlightGroup
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS HighlightGroup
readsPrec :: Int -> ReadS HighlightGroup
$creadList :: ReadS [HighlightGroup]
readList :: ReadS [HighlightGroup]
$creadPrec :: ReadPrec HighlightGroup
readPrec :: ReadPrec HighlightGroup
$creadListPrec :: ReadPrec [HighlightGroup]
readListPrec :: ReadPrec [HighlightGroup]
Read, Int -> HighlightGroup
HighlightGroup -> Int
HighlightGroup -> [HighlightGroup]
HighlightGroup -> HighlightGroup
HighlightGroup -> HighlightGroup -> [HighlightGroup]
HighlightGroup
-> HighlightGroup -> HighlightGroup -> [HighlightGroup]
(HighlightGroup -> HighlightGroup)
-> (HighlightGroup -> HighlightGroup)
-> (Int -> HighlightGroup)
-> (HighlightGroup -> Int)
-> (HighlightGroup -> [HighlightGroup])
-> (HighlightGroup -> HighlightGroup -> [HighlightGroup])
-> (HighlightGroup -> HighlightGroup -> [HighlightGroup])
-> (HighlightGroup
    -> HighlightGroup -> HighlightGroup -> [HighlightGroup])
-> Enum HighlightGroup
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: HighlightGroup -> HighlightGroup
succ :: HighlightGroup -> HighlightGroup
$cpred :: HighlightGroup -> HighlightGroup
pred :: HighlightGroup -> HighlightGroup
$ctoEnum :: Int -> HighlightGroup
toEnum :: Int -> HighlightGroup
$cfromEnum :: HighlightGroup -> Int
fromEnum :: HighlightGroup -> Int
$cenumFrom :: HighlightGroup -> [HighlightGroup]
enumFrom :: HighlightGroup -> [HighlightGroup]
$cenumFromThen :: HighlightGroup -> HighlightGroup -> [HighlightGroup]
enumFromThen :: HighlightGroup -> HighlightGroup -> [HighlightGroup]
$cenumFromTo :: HighlightGroup -> HighlightGroup -> [HighlightGroup]
enumFromTo :: HighlightGroup -> HighlightGroup -> [HighlightGroup]
$cenumFromThenTo :: HighlightGroup
-> HighlightGroup -> HighlightGroup -> [HighlightGroup]
enumFromThenTo :: HighlightGroup
-> HighlightGroup -> HighlightGroup -> [HighlightGroup]
Enum, HighlightGroup
HighlightGroup -> HighlightGroup -> Bounded HighlightGroup
forall a. a -> a -> Bounded a
$cminBound :: HighlightGroup
minBound :: HighlightGroup
$cmaxBound :: HighlightGroup
maxBound :: HighlightGroup
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 :: HighlightGroup -> Int64
priority HighlightGroup
CornelisError              = Int64
150
priority HighlightGroup
CornelisErrorWarning       = Int64
150
priority HighlightGroup
CornelisWarn               = Int64
150
priority HighlightGroup
CornelisUnsolvedMeta       = Int64
150
priority HighlightGroup
CornelisUnsolvedConstraint = Int64
150
priority HighlightGroup
_                          = Int64
100

atomToHlGroup :: Text -> Maybe HighlightGroup
atomToHlGroup :: Text -> Maybe HighlightGroup
atomToHlGroup Text
atom = Text -> Map Text HighlightGroup -> Maybe HighlightGroup
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
atom Map Text HighlightGroup
allHlGroups where
    stripCornelis :: Text -> Text
stripCornelis = Maybe Text -> Text
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Text -> Text) -> (Text -> Maybe Text) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> Maybe Text
T.stripPrefix Text
"Cornelis"

    toAtomName :: HighlightGroup -> Text
    toAtomName :: HighlightGroup -> Text
toAtomName HighlightGroup
hlGroup = Text -> Text
T.toLower (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Text -> Text
stripCornelis (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ HighlightGroup -> String
forall a. Show a => a -> String
show HighlightGroup
hlGroup

    allHlGroups :: M.Map Text HighlightGroup
    allHlGroups :: Map Text HighlightGroup
allHlGroups = [(Text, HighlightGroup)] -> Map Text HighlightGroup
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Text, HighlightGroup)] -> Map Text HighlightGroup)
-> [(Text, HighlightGroup)] -> Map Text HighlightGroup
forall a b. (a -> b) -> a -> b
$
        (HighlightGroup -> (Text, HighlightGroup))
-> [HighlightGroup] -> [(Text, HighlightGroup)]
forall a b. (a -> b) -> [a] -> [b]
map (\HighlightGroup
g -> (HighlightGroup -> Text
toAtomName HighlightGroup
g, HighlightGroup
g)) [(HighlightGroup
forall a. Bounded a => a
minBound :: HighlightGroup) ..]

data InfoHighlight a = InfoHighlight
  { forall a. InfoHighlight a -> (Int64, Int64)
ihl_start :: (Int64, Int64)
  , forall a. InfoHighlight a -> a
ihl_end :: a
  , forall a. InfoHighlight a -> HighlightGroup
ihl_group :: HighlightGroup
  }
  deriving (InfoHighlight a -> InfoHighlight a -> Bool
(InfoHighlight a -> InfoHighlight a -> Bool)
-> (InfoHighlight a -> InfoHighlight a -> Bool)
-> Eq (InfoHighlight a)
forall a. Eq a => InfoHighlight a -> InfoHighlight a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => InfoHighlight a -> InfoHighlight a -> Bool
== :: InfoHighlight a -> InfoHighlight a -> Bool
$c/= :: forall a. Eq a => InfoHighlight a -> InfoHighlight a -> Bool
/= :: InfoHighlight a -> InfoHighlight a -> Bool
Eq, Eq (InfoHighlight a)
Eq (InfoHighlight a) =>
(InfoHighlight a -> InfoHighlight a -> Ordering)
-> (InfoHighlight a -> InfoHighlight a -> Bool)
-> (InfoHighlight a -> InfoHighlight a -> Bool)
-> (InfoHighlight a -> InfoHighlight a -> Bool)
-> (InfoHighlight a -> InfoHighlight a -> Bool)
-> (InfoHighlight a -> InfoHighlight a -> InfoHighlight a)
-> (InfoHighlight a -> InfoHighlight a -> InfoHighlight a)
-> Ord (InfoHighlight a)
InfoHighlight a -> InfoHighlight a -> Bool
InfoHighlight a -> InfoHighlight a -> Ordering
InfoHighlight a -> InfoHighlight a -> InfoHighlight a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (InfoHighlight a)
forall a. Ord a => InfoHighlight a -> InfoHighlight a -> Bool
forall a. Ord a => InfoHighlight a -> InfoHighlight a -> Ordering
forall a.
Ord a =>
InfoHighlight a -> InfoHighlight a -> InfoHighlight a
$ccompare :: forall a. Ord a => InfoHighlight a -> InfoHighlight a -> Ordering
compare :: InfoHighlight a -> InfoHighlight a -> Ordering
$c< :: forall a. Ord a => InfoHighlight a -> InfoHighlight a -> Bool
< :: InfoHighlight a -> InfoHighlight a -> Bool
$c<= :: forall a. Ord a => InfoHighlight a -> InfoHighlight a -> Bool
<= :: InfoHighlight a -> InfoHighlight a -> Bool
$c> :: forall a. Ord a => InfoHighlight a -> InfoHighlight a -> Bool
> :: InfoHighlight a -> InfoHighlight a -> Bool
$c>= :: forall a. Ord a => InfoHighlight a -> InfoHighlight a -> Bool
>= :: InfoHighlight a -> InfoHighlight a -> Bool
$cmax :: forall a.
Ord a =>
InfoHighlight a -> InfoHighlight a -> InfoHighlight a
max :: InfoHighlight a -> InfoHighlight a -> InfoHighlight a
$cmin :: forall a.
Ord a =>
InfoHighlight a -> InfoHighlight a -> InfoHighlight a
min :: InfoHighlight a -> InfoHighlight a -> InfoHighlight a
Ord, Int -> InfoHighlight a -> ShowS
[InfoHighlight a] -> ShowS
InfoHighlight a -> String
(Int -> InfoHighlight a -> ShowS)
-> (InfoHighlight a -> String)
-> ([InfoHighlight a] -> ShowS)
-> Show (InfoHighlight a)
forall a. Show a => Int -> InfoHighlight a -> ShowS
forall a. Show a => [InfoHighlight a] -> ShowS
forall a. Show a => InfoHighlight a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> InfoHighlight a -> ShowS
showsPrec :: Int -> InfoHighlight a -> ShowS
$cshow :: forall a. Show a => InfoHighlight a -> String
show :: InfoHighlight a -> String
$cshowList :: forall a. Show a => [InfoHighlight a] -> ShowS
showList :: [InfoHighlight a] -> ShowS
Show, (forall a b. (a -> b) -> InfoHighlight a -> InfoHighlight b)
-> (forall a b. a -> InfoHighlight b -> InfoHighlight a)
-> Functor InfoHighlight
forall a b. a -> InfoHighlight b -> InfoHighlight a
forall a b. (a -> b) -> InfoHighlight a -> InfoHighlight b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> InfoHighlight a -> InfoHighlight b
fmap :: forall a b. (a -> b) -> InfoHighlight a -> InfoHighlight b
$c<$ :: forall a b. a -> InfoHighlight b -> InfoHighlight a
<$ :: forall a b. a -> InfoHighlight b -> InfoHighlight a
Functor)

spanInfoHighlights
    :: InfoHighlight (Int64, Int64)
    -> [InfoHighlight Int64]
spanInfoHighlights :: InfoHighlight (Int64, Int64) -> [InfoHighlight Int64]
spanInfoHighlights ih :: InfoHighlight (Int64, Int64)
ih@(InfoHighlight (Int64
sl, Int64
sc) (Int64
el, Int64
ec) HighlightGroup
hg)
  | Int64
sl Int64 -> Int64 -> Bool
forall a. Eq a => a -> a -> Bool
== Int64
el = InfoHighlight Int64 -> [InfoHighlight Int64]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (InfoHighlight Int64 -> [InfoHighlight Int64])
-> InfoHighlight Int64 -> [InfoHighlight Int64]
forall a b. (a -> b) -> a -> b
$ ((Int64, Int64) -> Int64)
-> InfoHighlight (Int64, Int64) -> InfoHighlight Int64
forall a b. (a -> b) -> InfoHighlight a -> InfoHighlight b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int64, Int64) -> Int64
forall a b. (a, b) -> b
snd InfoHighlight (Int64, Int64)
ih
  | Bool
otherwise
      = (Int64, Int64) -> Int64 -> HighlightGroup -> InfoHighlight Int64
forall a. (Int64, Int64) -> a -> HighlightGroup -> InfoHighlight a
InfoHighlight (Int64
sl, Int64
sc) (-Int64
1) HighlightGroup
hg
      InfoHighlight Int64
-> [InfoHighlight Int64] -> [InfoHighlight Int64]
forall a. a -> [a] -> [a]
: (Int64, Int64) -> Int64 -> HighlightGroup -> InfoHighlight Int64
forall a. (Int64, Int64) -> a -> HighlightGroup -> InfoHighlight a
InfoHighlight (Int64
el, Int64
0) Int64
ec HighlightGroup
hg
      InfoHighlight Int64
-> [InfoHighlight Int64] -> [InfoHighlight Int64]
forall a. a -> [a] -> [a]
: (Int64 -> InfoHighlight Int64) -> [Int64] -> [InfoHighlight Int64]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Int64
l -> (Int64, Int64) -> Int64 -> HighlightGroup -> InfoHighlight Int64
forall a. (Int64, Int64) -> a -> HighlightGroup -> InfoHighlight a
InfoHighlight (Int64
l, Int64
0) (-Int64
1) HighlightGroup
hg) [Int64
sl Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
1 .. Int64
el Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
- Int64
1]


renderWithHlGroups
    :: SimpleDocStream HighlightGroup
    -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
renderWithHlGroups :: forall a.
SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
renderWithHlGroups = [InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a.
[InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
go [] Int64
0 Int64
0
  where
    go
      :: [InfoHighlight ()]
      -> Int64
      -> Int64
      -> SimpleDocStream HighlightGroup
      -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
    go :: forall a.
[InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
go [InfoHighlight ()]
_ Int64
_ Int64
_ SimpleDocStream HighlightGroup
SFail = SimpleDocStream a
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a. a -> ([InfoHighlight (Int64, Int64)], a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SimpleDocStream a
forall ann. SimpleDocStream ann
SFail
    go [InfoHighlight ()]
_ Int64
_ Int64
_ SimpleDocStream HighlightGroup
SEmpty = SimpleDocStream a
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a. a -> ([InfoHighlight (Int64, Int64)], a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure SimpleDocStream a
forall ann. SimpleDocStream ann
SEmpty
    go [InfoHighlight ()]
st Int64
r Int64
c (SChar Char
c' SimpleDocStream HighlightGroup
sds) =
      Char -> SimpleDocStream a -> SimpleDocStream a
forall ann. Char -> SimpleDocStream ann -> SimpleDocStream ann
SChar Char
c' (SimpleDocStream a -> SimpleDocStream a)
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a.
[InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
go [InfoHighlight ()]
st Int64
r (Int64
c Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Char -> Int
charToBytes Char
c')) SimpleDocStream HighlightGroup
sds
    go [InfoHighlight ()]
st Int64
r Int64
c (SText Int
n Text
txt SimpleDocStream HighlightGroup
sds) =
      Int -> Text -> SimpleDocStream a -> SimpleDocStream a
forall ann.
Int -> Text -> SimpleDocStream ann -> SimpleDocStream ann
SText Int
n Text
txt (SimpleDocStream a -> SimpleDocStream a)
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a.
[InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
go [InfoHighlight ()]
st Int64
r (Int64
c Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Text -> Int
textToBytes Text
txt)) SimpleDocStream HighlightGroup
sds
    go [InfoHighlight ()]
st Int64
r Int64
_ (SLine Int
n SimpleDocStream HighlightGroup
sds) = Int -> SimpleDocStream a -> SimpleDocStream a
forall ann. Int -> SimpleDocStream ann -> SimpleDocStream ann
SLine Int
n (SimpleDocStream a -> SimpleDocStream a)
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a.
[InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
go [InfoHighlight ()]
st (Int64
r Int64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+ Int64
1) (Int -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) SimpleDocStream HighlightGroup
sds
    go [InfoHighlight ()]
st Int64
r Int64
c (SAnnPush HighlightGroup
hg SimpleDocStream HighlightGroup
sds) = [InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a.
[InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
go ((Int64, Int64) -> () -> HighlightGroup -> InfoHighlight ()
forall a. (Int64, Int64) -> a -> HighlightGroup -> InfoHighlight a
InfoHighlight (Int64
r, Int64
c) () HighlightGroup
hg InfoHighlight () -> [InfoHighlight ()] -> [InfoHighlight ()]
forall a. a -> [a] -> [a]
: [InfoHighlight ()]
st) Int64
r Int64
c SimpleDocStream HighlightGroup
sds
    go [] Int64
_ Int64
_ (SAnnPop SimpleDocStream HighlightGroup
_) = String -> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a. HasCallStack => String -> a
error String
"popping an annotation that doesn't exist"
    go (InfoHighlight ()
ih : [InfoHighlight ()]
ihs) Int64
r Int64
c (SAnnPop SimpleDocStream HighlightGroup
sds) = do
      SimpleDocStream a
sds' <- [InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
forall a.
[InfoHighlight ()]
-> Int64
-> Int64
-> SimpleDocStream HighlightGroup
-> ([InfoHighlight (Int64, Int64)], SimpleDocStream a)
go [InfoHighlight ()]
ihs Int64
r Int64
c SimpleDocStream HighlightGroup
sds
      ([(Int64
r, Int64
c) (Int64, Int64) -> InfoHighlight () -> InfoHighlight (Int64, Int64)
forall a b. a -> InfoHighlight b -> InfoHighlight a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ InfoHighlight ()
ih], SimpleDocStream a
sds')


prettyType :: C.Type -> Doc HighlightGroup
prettyType :: Type -> Doc HighlightGroup
prettyType (C.Type Text
ty) = HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisType (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
sep ([Doc HighlightGroup] -> Doc HighlightGroup)
-> [Doc HighlightGroup] -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ (Text -> Doc HighlightGroup) -> [Text] -> [Doc HighlightGroup]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty ([Text] -> [Doc HighlightGroup]) -> [Text] -> [Doc HighlightGroup]
forall a b. (a -> b) -> a -> b
$ Text -> [Text]
T.lines Text
ty


groupScopeSet :: [InScope] -> [[InScope]]
groupScopeSet :: [InScope] -> [[InScope]]
groupScopeSet
  = ([InScope] -> Text) -> [[InScope]] -> [[InScope]]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (InScope -> Text
is_refied_name (InScope -> Text) -> ([InScope] -> InScope) -> [InScope] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [InScope] -> InScope
forall a. HasCallStack => [a] -> a
head)
  ([[InScope]] -> [[InScope]])
-> ([InScope] -> [[InScope]]) -> [InScope] -> [[InScope]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([InScope] -> [InScope]) -> [[InScope]] -> [[InScope]]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((InScope -> Text) -> [InScope] -> [InScope]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn InScope -> Text
is_refied_name)
  ([[InScope]] -> [[InScope]])
-> ([InScope] -> [[InScope]]) -> [InScope] -> [[InScope]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InScope -> InScope -> Bool) -> [InScope] -> [[InScope]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy ((Type -> Type -> Bool)
-> (InScope -> Type) -> InScope -> InScope -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
(==) InScope -> Type
is_type)
  ([InScope] -> [[InScope]])
-> ([InScope] -> [InScope]) -> [InScope] -> [[InScope]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InScope -> Type) -> [InScope] -> [InScope]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn InScope -> Type
is_type

prettyGoals :: DisplayInfo -> Doc HighlightGroup
prettyGoals :: DisplayInfo -> Doc HighlightGroup
prettyGoals (AllGoalsWarnings [GoalInfo (InteractionPoint Identity)]
vis [GoalInfo NamedPoint]
invis [Message]
errs [Message]
warns) =
  [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
vcat ([Doc HighlightGroup] -> Doc HighlightGroup)
-> [Doc HighlightGroup] -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Doc HighlightGroup -> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc HighlightGroup
forall ann. Doc ann
hardline ([Doc HighlightGroup] -> [Doc HighlightGroup])
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a b. (a -> b) -> a -> b
$ (Doc HighlightGroup -> Bool)
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Doc HighlightGroup -> Bool) -> Doc HighlightGroup -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc HighlightGroup -> Bool
isEmpty)
    [ Doc HighlightGroup
-> [Message]
-> (Message -> Doc HighlightGroup)
-> Doc HighlightGroup
forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
"Warnings" [Message]
warns ((Message -> Doc HighlightGroup) -> Doc HighlightGroup)
-> (Message -> Doc HighlightGroup) -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisWarn (Doc HighlightGroup -> Doc HighlightGroup)
-> (Message -> Doc HighlightGroup) -> Message -> Doc HighlightGroup
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc HighlightGroup)
-> (Message -> Text) -> Message -> Doc HighlightGroup
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Message -> Text
getMessage
    , Doc HighlightGroup
-> [GoalInfo (InteractionPoint Identity)]
-> (GoalInfo (InteractionPoint Identity) -> Doc HighlightGroup)
-> Doc HighlightGroup
forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
"Visible Goals" [GoalInfo (InteractionPoint Identity)]
vis ((GoalInfo (InteractionPoint Identity) -> Doc HighlightGroup)
 -> Doc HighlightGroup)
-> (GoalInfo (InteractionPoint Identity) -> Doc HighlightGroup)
-> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$
        GoalInfo Text -> Doc HighlightGroup
prettyGoal (GoalInfo Text -> Doc HighlightGroup)
-> (GoalInfo (InteractionPoint Identity) -> GoalInfo Text)
-> GoalInfo (InteractionPoint Identity)
-> Doc HighlightGroup
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InteractionPoint Identity -> Text)
-> GoalInfo (InteractionPoint Identity) -> GoalInfo Text
forall a b. (a -> b) -> GoalInfo a -> GoalInfo b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Text -> Text
forall a. Monoid a => a -> a -> a
mappend Text
"?" (Text -> Text)
-> (InteractionPoint Identity -> Text)
-> InteractionPoint Identity
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> Text)
-> (InteractionPoint Identity -> String)
-> InteractionPoint Identity
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionId -> String
forall a. Show a => a -> String
show (InteractionId -> String)
-> (InteractionPoint Identity -> InteractionId)
-> InteractionPoint Identity
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InteractionPoint Identity -> InteractionId
forall (f :: * -> *). InteractionPoint f -> InteractionId
ip_id)
    , Doc HighlightGroup
-> [Message]
-> (Message -> Doc HighlightGroup)
-> Doc HighlightGroup
forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
"Errors" [Message]
errs Message -> Doc HighlightGroup
prettyError
    , Doc HighlightGroup
-> [GoalInfo NamedPoint]
-> (GoalInfo NamedPoint -> Doc HighlightGroup)
-> Doc HighlightGroup
forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
"Invisible Goals" [GoalInfo NamedPoint]
invis ((GoalInfo NamedPoint -> Doc HighlightGroup) -> Doc HighlightGroup)
-> (GoalInfo NamedPoint -> Doc HighlightGroup)
-> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ \GoalInfo NamedPoint
gi ->
        GoalInfo Text -> Doc HighlightGroup
prettyGoal ((NamedPoint -> Text) -> GoalInfo NamedPoint -> GoalInfo Text
forall a b. (a -> b) -> GoalInfo a -> GoalInfo b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedPoint -> Text
np_name GoalInfo NamedPoint
gi)
          Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc HighlightGroup
-> (AgdaInterval -> Doc HighlightGroup)
-> Maybe AgdaInterval
-> Doc HighlightGroup
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc HighlightGroup
forall a. Monoid a => a
mempty (Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann
brackets (Doc HighlightGroup -> Doc HighlightGroup)
-> (AgdaInterval -> Doc HighlightGroup)
-> AgdaInterval
-> Doc HighlightGroup
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Doc HighlightGroup
"at" <+>) (Doc HighlightGroup -> Doc HighlightGroup)
-> (AgdaInterval -> Doc HighlightGroup)
-> AgdaInterval
-> Doc HighlightGroup
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AgdaInterval -> Doc HighlightGroup
prettyInterval) (NamedPoint -> Maybe AgdaInterval
np_interval (NamedPoint -> Maybe AgdaInterval)
-> NamedPoint -> Maybe AgdaInterval
forall a b. (a -> b) -> a -> b
$ GoalInfo NamedPoint -> NamedPoint
forall a. GoalInfo a -> a
gi_ip GoalInfo NamedPoint
gi)
    ]
prettyGoals (GoalSpecific InteractionPoint Identity
_ [InScope]
scoped Type
ty Maybe Type
mhave Maybe [Text]
mboundary Maybe [Text]
mconstraints) =
  [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
vcat ([Doc HighlightGroup] -> Doc HighlightGroup)
-> [Doc HighlightGroup] -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Doc HighlightGroup -> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. a -> [a] -> [a]
intersperse (forall a b. (Semigroup a, Integral b) => b -> a -> a
stimes @_ @Int Int
60 Doc HighlightGroup
"—") ([Doc HighlightGroup] -> [Doc HighlightGroup])
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a b. (a -> b) -> a -> b
$
    [ Doc HighlightGroup
-> [Text] -> (Text -> Doc HighlightGroup) -> Doc HighlightGroup
forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
"Boundary" ([Text] -> Maybe [Text] -> [Text]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Text]
mboundary) Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty
    ] [Doc HighlightGroup]
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. Semigroup a => a -> a -> a
<>
    [ HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisTitle Doc HighlightGroup
"Goal:" Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc HighlightGroup
prettyType Type
ty
    ] [Doc HighlightGroup]
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. Semigroup a => a -> a -> a
<>
    [ HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisTitle Doc HighlightGroup
"Have:" Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc HighlightGroup
prettyType Type
have
    | Type
have <- Maybe Type -> [Type]
forall a. Maybe a -> [a]
maybeToList Maybe Type
mhave
    ] [Doc HighlightGroup]
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. Semigroup a => a -> a -> a
<>
    [ [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
vcat ([Doc HighlightGroup] -> Doc HighlightGroup)
-> [Doc HighlightGroup] -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ ([InScope] -> Doc HighlightGroup)
-> [[InScope]] -> [Doc HighlightGroup]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [InScope] -> Doc HighlightGroup
prettyInScopeSet ([[InScope]] -> [Doc HighlightGroup])
-> [[InScope]] -> [Doc HighlightGroup]
forall a b. (a -> b) -> a -> b
$ [InScope] -> [[InScope]]
groupScopeSet [InScope]
scoped
    ] [Doc HighlightGroup]
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. Semigroup a => a -> a -> a
<>
    [ Doc HighlightGroup
-> [Text] -> (Text -> Doc HighlightGroup) -> Doc HighlightGroup
forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
"Constraints" ([Text] -> Maybe [Text] -> [Text]
forall a. a -> Maybe a -> a
fromMaybe [] Maybe [Text]
mconstraints) Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty
    ]
prettyGoals (HelperFunction Text
sig) =
  Doc HighlightGroup
-> [Doc HighlightGroup]
-> (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup
forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
"Helper Function"
    [ Doc HighlightGroup
forall a. Monoid a => a
mempty
    , HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisType (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
sig
    , Doc HighlightGroup
forall a. Monoid a => a
mempty
    , HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisComment (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann
parens Doc HighlightGroup
"copied to \" register"
    ] Doc HighlightGroup -> Doc HighlightGroup
forall a. a -> a
id
prettyGoals (InferredType Type
ty) =
  HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisTitle Doc HighlightGroup
"Inferred Type:" Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Type -> Doc HighlightGroup
prettyType Type
ty
prettyGoals (WhyInScope Text
msg) = Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
msg
prettyGoals (NormalForm Text
expr) = Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
expr
prettyGoals (DisplayError Text
err) = HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisError (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
err
prettyGoals (UnknownDisplayInfo Value
v) = HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisError (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ String -> Doc HighlightGroup
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc HighlightGroup) -> String -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Value -> String
forall a. Show a => a -> String
show Value
v

prettyInterval :: AgdaInterval -> Doc HighlightGroup
prettyInterval :: AgdaInterval -> Doc HighlightGroup
prettyInterval (Interval AgdaPos
s AgdaPos
e)
  | AgdaPos -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line AgdaPos
s Index 'Line 'OneIndexed -> Index 'Line 'OneIndexed -> Bool
forall a. Eq a => a -> a -> Bool
== AgdaPos -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line AgdaPos
e
  = AgdaPos -> Doc HighlightGroup
prettyPoint AgdaPos
s Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Doc HighlightGroup
"-" Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Index 'CodePoint 'OneIndexed -> Doc HighlightGroup
forall a ann. Pretty a => a -> Doc ann
forall ann. Index 'CodePoint 'OneIndexed -> Doc ann
pretty (AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
e)
  | Bool
otherwise
  = AgdaPos -> Doc HighlightGroup
prettyPoint AgdaPos
s Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Doc HighlightGroup
"-" Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> AgdaPos -> Doc HighlightGroup
prettyPoint AgdaPos
e

prettyPoint :: AgdaPos -> Doc HighlightGroup
prettyPoint :: AgdaPos -> Doc HighlightGroup
prettyPoint AgdaPos
p = Index 'Line 'OneIndexed -> Doc HighlightGroup
forall a ann. Pretty a => a -> Doc ann
forall ann. Index 'Line 'OneIndexed -> Doc ann
pretty (AgdaPos -> Index 'Line 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index 'Line i
p_line AgdaPos
p) Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Doc HighlightGroup
"," Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Index 'CodePoint 'OneIndexed -> Doc HighlightGroup
forall a ann. Pretty a => a -> Doc ann
forall ann. Index 'CodePoint 'OneIndexed -> Doc ann
pretty (AgdaPos -> Index 'CodePoint 'OneIndexed
forall (e :: Unit) (i :: Indexing) (j :: Indexing).
Pos e i j -> Index e j
p_col AgdaPos
p)


isEmpty :: Doc HighlightGroup -> Bool
isEmpty :: Doc HighlightGroup -> Bool
isEmpty Doc HighlightGroup
Empty = Bool
True
isEmpty Doc HighlightGroup
_ = Bool
False


section
    :: Doc HighlightGroup
    -> [a]
    -> (a -> Doc HighlightGroup)
    -> Doc HighlightGroup
section :: forall a.
Doc HighlightGroup
-> [a] -> (a -> Doc HighlightGroup) -> Doc HighlightGroup
section Doc HighlightGroup
_ [] a -> Doc HighlightGroup
_ = Doc HighlightGroup
forall a. Monoid a => a
mempty
section Doc HighlightGroup
doc [a]
as a -> Doc HighlightGroup
f = [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
vcat ([Doc HighlightGroup] -> Doc HighlightGroup)
-> [Doc HighlightGroup] -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$
  HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisTitle (Doc HighlightGroup
doc Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Doc HighlightGroup
":") Doc HighlightGroup -> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. a -> [a] -> [a]
: (a -> Doc HighlightGroup) -> [a] -> [Doc HighlightGroup]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc HighlightGroup
f [a]
as


prettyName :: Text -> Doc HighlightGroup
prettyName :: Text -> Doc HighlightGroup
prettyName = Bool -> Text -> Doc HighlightGroup
prettyVisibleName Bool
True


prettyVisibleName :: Bool -> Text -> Doc HighlightGroup
prettyVisibleName :: Bool -> Text -> Doc HighlightGroup
prettyVisibleName Bool
False Text
t = HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisComment (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Doc HighlightGroup
"(" Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
t Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall a. Semigroup a => a -> a -> a
<> Doc HighlightGroup
")"
prettyVisibleName Bool
True Text
t = HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisName (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
t

prettyInScope :: InScope -> Doc HighlightGroup
prettyInScope :: InScope -> Doc HighlightGroup
prettyInScope (InScope Text
reified Text
_ Bool
in_scope Type
ty) =
  [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
hsep
    [ GoalInfo Text -> Doc HighlightGroup
prettyGoal (GoalInfo Text -> Doc HighlightGroup)
-> GoalInfo Text -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ Text -> Type -> GoalInfo Text
forall a. a -> Type -> GoalInfo a
GoalInfo Text
reified Type
ty
    , Doc HighlightGroup
-> Doc HighlightGroup -> Bool -> Doc HighlightGroup
forall a. a -> a -> Bool -> a
bool
        (String -> Doc HighlightGroup
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
6 Char
' ') Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann -> Doc ann
<+> HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisComment (Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann
parens Doc HighlightGroup
"not in scope"))
        Doc HighlightGroup
forall a. Monoid a => a
mempty
        Bool
in_scope
    ]

prettyInScopeSet :: [InScope] -> Doc HighlightGroup
prettyInScopeSet :: [InScope] -> Doc HighlightGroup
prettyInScopeSet [InScope]
is =
  let ty :: Type
ty = InScope -> Type
is_type (InScope -> Type) -> InScope -> Type
forall a b. (a -> b) -> a -> b
$ [InScope] -> InScope
forall a. HasCallStack => [a] -> a
head [InScope]
is
   in [InScope] -> Type -> Doc HighlightGroup
prettyManyGoals [InScope]
is Type
ty

prettyManyGoals :: [InScope] -> X.Type -> Doc HighlightGroup
prettyManyGoals :: [InScope] -> Type -> Doc HighlightGroup
prettyManyGoals [InScope]
is Type
ty =
  Int -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Int -> Doc ann -> Doc ann
hang Int
4 (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
sep
    [ [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
hsep ([Doc HighlightGroup] -> Doc HighlightGroup)
-> [Doc HighlightGroup] -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$
        (InScope -> Doc HighlightGroup)
-> [InScope] -> [Doc HighlightGroup]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\InScope
i -> Bool -> Text -> Doc HighlightGroup
prettyVisibleName (InScope -> Bool
is_in_scope InScope
i) (Text -> Doc HighlightGroup) -> Text -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ InScope -> Text
is_refied_name InScope
i) [InScope]
is [Doc HighlightGroup]
-> [Doc HighlightGroup] -> [Doc HighlightGroup]
forall a. Semigroup a => a -> a -> a
<> [Doc HighlightGroup
":"]
    , Type -> Doc HighlightGroup
prettyType Type
ty
    ]

prettyGoal :: GoalInfo Text -> Doc HighlightGroup
prettyGoal :: GoalInfo Text -> Doc HighlightGroup
prettyGoal (GoalInfo Text
name Type
ty) =
  Int -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Int -> Doc ann -> Doc ann
hang Int
4 (Doc HighlightGroup -> Doc HighlightGroup)
-> Doc HighlightGroup -> Doc HighlightGroup
forall a b. (a -> b) -> a -> b
$ [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
sep
    [ Text -> Doc HighlightGroup
prettyName Text
name Doc HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc HighlightGroup
":"
    , Type -> Doc HighlightGroup
prettyType Type
ty
    ]

prettyError :: Message -> Doc HighlightGroup
prettyError :: Message -> Doc HighlightGroup
prettyError (Message Text
msg) =
  let (Text
hdr, Text
body) = (Text -> Text) -> (Text, Text) -> (Text, Text)
forall a b. (a -> b) -> (Text, a) -> (Text, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> Text -> Text
T.drop Int
1) ((Text, Text) -> (Text, Text)) -> (Text, Text) -> (Text, Text)
forall a b. (a -> b) -> a -> b
$ (Char -> Bool) -> Text -> (Text, Text)
T.break (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n') Text
msg in
  [Doc HighlightGroup] -> Doc HighlightGroup
forall ann. [Doc ann] -> Doc ann
vcat [ HighlightGroup -> Doc HighlightGroup -> Doc HighlightGroup
forall ann. ann -> Doc ann -> Doc ann
annotate HighlightGroup
CornelisError (Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
hdr) , Text -> Doc HighlightGroup
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Text
body ]