{-# LANGUAGE CPP #-}

-- | A simple document tree to render @'Doc' ann@ but preserve annotations.
--
-- 'DocTree' and 'renderToTree'' originally taken from
-- <https://github.com/plt-amy/agda/blob/9fd50b883f14a05792ed79a0b693fbecb2165bf5/src/full/Agda/LSP/Output.hs>
-- but rewritten to encode more invariants.

module Agda.Utils.DocTree
  ( DocTree( Node, Text )
  , prettyDocTree
  , renderToTree
  , renderToTree'
  , renderTree'
  , treeToText
  , treeToTextNoAnn
  , treeToTextWithAnn
  )
where

import Prelude hiding (null)

import Control.DeepSeq    (NFData(..))
import Data.Text          (Text)
import Data.Text          qualified as Text
#if MIN_VERSION_text(2,0,2)
import Data.Text.Encoding (strictBuilderToText, textToStrictBuilder)
import Data.Text.Encoding qualified
#else
-- GHC 9.2 ships text-1.2.5.0
import Data.Text.Lazy qualified as TL
import Data.Text.Lazy.Builder qualified as Builder
#endif

import GHC.Generics

import Text.PrettyPrint.Annotated.HughesPJ (Doc)
import Text.PrettyPrint.Annotated.HughesPJ qualified as Ppr

import Agda.Utils.Function (applyUnless)
import Agda.Utils.List1 (List1, pattern (:|), (<|))
import Agda.Utils.List1 qualified as List1
import Agda.Utils.Monoid (Fwd, pattern Fwd, appFwd)
import Agda.Utils.Null
import Agda.Utils.Range (Range(..))
import Agda.Utils.RangeMap (RangeMap)
import Agda.Utils.RangeMap qualified as RangeMap
import Agda.Utils.Singleton

import Agda.Utils.Impossible

-- | A rendered document with annotations from type @ann@.
data DocTree ann
  = Node ann [DocTree ann]
     -- ^ Stuff annotated by @ann@.
  | Text Text
     -- ^ Atom.
  deriving ((forall x. DocTree ann -> Rep (DocTree ann) x)
-> (forall x. Rep (DocTree ann) x -> DocTree ann)
-> Generic (DocTree ann)
forall x. Rep (DocTree ann) x -> DocTree ann
forall x. DocTree ann -> Rep (DocTree ann) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall ann x. Rep (DocTree ann) x -> DocTree ann
forall ann x. DocTree ann -> Rep (DocTree ann) x
$cfrom :: forall ann x. DocTree ann -> Rep (DocTree ann) x
from :: forall x. DocTree ann -> Rep (DocTree ann) x
$cto :: forall ann x. Rep (DocTree ann) x -> DocTree ann
to :: forall x. Rep (DocTree ann) x -> DocTree ann
Generic, Int -> DocTree ann -> ShowS
[DocTree ann] -> ShowS
DocTree ann -> String
(Int -> DocTree ann -> ShowS)
-> (DocTree ann -> String)
-> ([DocTree ann] -> ShowS)
-> Show (DocTree ann)
forall ann. Show ann => Int -> DocTree ann -> ShowS
forall ann. Show ann => [DocTree ann] -> ShowS
forall ann. Show ann => DocTree ann -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall ann. Show ann => Int -> DocTree ann -> ShowS
showsPrec :: Int -> DocTree ann -> ShowS
$cshow :: forall ann. Show ann => DocTree ann -> String
show :: DocTree ann -> String
$cshowList :: forall ann. Show ann => [DocTree ann] -> ShowS
showList :: [DocTree ann] -> ShowS
Show)

instance Null (DocTree ann) where
  empty :: DocTree ann
empty = Text -> DocTree ann
forall ann. Text -> DocTree ann
Text Text
forall a. Monoid a => a
mempty
  null :: DocTree ann -> Bool
null = \case
    Node ann
a [DocTree ann]
ts -> (DocTree ann -> Bool) -> [DocTree ann] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all DocTree ann -> Bool
forall a. Null a => a -> Bool
null [DocTree ann]
ts
    Text Text
t    -> Text -> Bool
forall a. Null a => a -> Bool
null Text
t

instance NFData ann => NFData (DocTree ann) where

---------------------------------------------------------------------------
-- * Converting 'DocTree' to 'Doc'

prettyDocTree :: DocTree ann -> Doc ann
prettyDocTree :: forall ann. DocTree ann -> Doc ann
prettyDocTree = \case
  Text Text
t    -> String -> Doc ann
forall a. String -> Doc a
Ppr.text (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack Text
t  -- Bad, we should have a Doc that supports Text
  Node ann
a [DocTree ann]
ts -> ann -> Doc ann -> Doc ann
forall a. a -> Doc a -> Doc a
Ppr.annotate ann
a (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall a b. (a -> b) -> a -> b
$ (DocTree ann -> Doc ann) -> [DocTree ann] -> Doc ann
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap DocTree ann -> Doc ann
forall ann. DocTree ann -> Doc ann
prettyDocTree [DocTree ann]
ts

---------------------------------------------------------------------------
-- * Converting 'Doc' to 'DocTree'
--
-- Implemented as state machine where the state is a stack of unclosed
-- annotation with the annotated stuff inbetween.

-- | State of the right-to-left conversion to tree.
data St ann = St
  { forall ann. St ann -> String
front :: String
      -- ^ Accumulator for text.
  , forall ann. St ann -> List1 (Item ann)
stack :: List1 (Item ann)
      -- ^ A nonempty stack of annotated trees with their closing annotation bracket,
      --   waiting for the opening bracket.
  }

-- | Annotated stuff waiting for the opening bracket.
data Item ann = Item ann [DocTree ann]

-- Initial state.
instance Null ann => Null (St ann) where
  empty :: St ann
empty = String -> List1 (Item ann) -> St ann
forall ann. String -> List1 (Item ann) -> St ann
St String
forall a. Null a => a
empty (Item ann -> List1 (Item ann)
forall a. a -> NonEmpty a
List1.singleton Item ann
forall a. Null a => a
empty)
  null :: St ann -> Bool
null (St String
s List1 (Item ann)
is) = String -> Bool
forall a. Null a => a -> Bool
null String
s Bool -> Bool -> Bool
&& (Item ann -> Bool) -> List1 (Item ann) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Item ann -> Bool
forall a. Null a => a -> Bool
null List1 (Item ann)
is

instance Null ann => Null (Item ann) where
  empty :: Item ann
empty = ann -> [DocTree ann] -> Item ann
forall ann. ann -> [DocTree ann] -> Item ann
Item ann
forall a. Null a => a
empty [DocTree ann]
forall a. Null a => a
empty
  null :: Item ann -> Bool
null (Item ann
a [DocTree ann]
ts) = ann -> Bool
forall a. Null a => a -> Bool
null ann
a Bool -> Bool -> Bool
&& [DocTree ann] -> Bool
forall a. Null a => a -> Bool
null [DocTree ann]
ts

type Width = Int
type Fill  = Float

-- | Render a @'Doc' ann@ to a @'DocTree' ann@ with the given layout parameters.
-- E.g. @width=100@ @fill=1.5@.
--
renderToTree' :: forall ann. Null ann => Width -> Fill -> Doc ann -> DocTree ann
renderToTree' :: forall ann. Null ann => Int -> Fill -> Doc ann -> DocTree ann
renderToTree' Int
width Fill
fill =
    St ann -> DocTree ann
finalize (St ann -> DocTree ann)
-> (Doc ann -> St ann) -> Doc ann -> DocTree ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Mode
-> Int
-> Fill
-> (AnnotDetails ann -> St ann -> St ann)
-> St ann
-> Doc ann
-> St ann
forall b a.
Mode
-> Int -> Fill -> (AnnotDetails b -> a -> a) -> a -> Doc b -> a
Ppr.fullRenderAnn Mode
Ppr.PageMode Int
width Fill
fill AnnotDetails ann -> St ann -> St ann
go St ann
forall a. Null a => a
empty
  where
    -- State machine transition for the right-to-left automaton.
    go :: Ppr.AnnotDetails ann -> St ann -> St ann
    go :: AnnotDetails ann -> St ann -> St ann
go = \case
      AnnotDetails ann
Ppr.AnnotStart  -> St ann -> St ann
annotStart
      Ppr.NoAnnot TextDetails
d Int
_ -> TextDetails -> St ann -> St ann
noAnnot TextDetails
d
      Ppr.AnnotEnd ann
a  -> ann -> St ann -> St ann
annotEnd ann
a

    finalize :: St ann -> DocTree ann
    finalize :: St ann -> DocTree ann
finalize (St String
s (Item ann
a [DocTree ann]
ts :| [Item ann]
is))
      | [Item ann] -> Bool
forall a. Null a => a -> Bool
null [Item ann]
is   = ann -> String -> [DocTree ann] -> DocTree ann
mkNode ann
a String
s [DocTree ann]
ts
      | Bool
otherwise = DocTree ann
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not well-bracketed

    -- Create a node once the opening bracket has been reached.
    mkNode :: ann -> String -> [DocTree ann] -> DocTree ann
    mkNode :: ann -> String -> [DocTree ann] -> DocTree ann
mkNode ann
a String
s [DocTree ann]
ts = ann -> [DocTree ann] -> DocTree ann
forall ann. ann -> [DocTree ann] -> DocTree ann
Node ann
a ([DocTree ann] -> DocTree ann) -> [DocTree ann] -> DocTree ann
forall a b. (a -> b) -> a -> b
$ Bool
-> ([DocTree ann] -> [DocTree ann])
-> [DocTree ann]
-> [DocTree ann]
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (String -> Bool
forall a. Null a => a -> Bool
null String
s) (Text -> DocTree ann
forall ann. Text -> DocTree ann
Text (String -> Text
Text.pack String
s) DocTree ann -> [DocTree ann] -> [DocTree ann]
forall a. a -> [a] -> [a]
:) [DocTree ann]
ts

    -- Got the opening bracket on an annotation:
    -- Pop an item from the stack
    annotStart :: St ann -> St ann
    annotStart :: St ann -> St ann
annotStart (St String
s (Item ann
a [DocTree ann]
ts :| [Item ann]
is1)) =
      case [Item ann]
is1 of
        Item ann
i : [Item ann]
is -> String -> NonEmpty (Item ann) -> St ann
forall ann. String -> List1 (Item ann) -> St ann
St String
"" (DocTree ann -> Item ann -> Item ann
consTree (ann -> String -> [DocTree ann] -> DocTree ann
mkNode ann
a String
s [DocTree ann]
ts) Item ann
i Item ann -> [Item ann] -> NonEmpty (Item ann)
forall a. a -> [a] -> NonEmpty a
:| [Item ann]
is)
        []     -> St ann
forall a. HasCallStack => a
__IMPOSSIBLE__  -- not well-bracketed
      where
        consTree :: DocTree ann -> Item ann -> Item ann
        consTree :: DocTree ann -> Item ann -> Item ann
consTree DocTree ann
t (Item ann
a [DocTree ann]
ts) = ann -> [DocTree ann] -> Item ann
forall ann. ann -> [DocTree ann] -> Item ann
Item ann
a (DocTree ann
t DocTree ann -> [DocTree ann] -> [DocTree ann]
forall a. a -> [a] -> [a]
: [DocTree ann]
ts)

    -- Got text.
    noAnnot :: Ppr.TextDetails -> St ann -> St ann
    noAnnot :: TextDetails -> St ann -> St ann
noAnnot (Ppr.Chr  Char
c) (St String
s0 NonEmpty (Item ann)
is) = String -> NonEmpty (Item ann) -> St ann
forall ann. String -> List1 (Item ann) -> St ann
St (Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: String
s0) NonEmpty (Item ann)
is
    noAnnot (Ppr.Str  String
s) (St String
s0 NonEmpty (Item ann)
is) = String -> NonEmpty (Item ann) -> St ann
forall ann. String -> List1 (Item ann) -> St ann
St (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s0) NonEmpty (Item ann)
is
    noAnnot (Ppr.PStr String
s) (St String
s0 NonEmpty (Item ann)
is) = String -> NonEmpty (Item ann) -> St ann
forall ann. String -> List1 (Item ann) -> St ann
St (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s0) NonEmpty (Item ann)
is

    -- Got the closing bracket of a new annotation:
    -- Push a new item on the stack.
    annotEnd :: ann -> St ann -> St ann
    annotEnd :: ann -> St ann -> St ann
annotEnd ann
a (St String
s NonEmpty (Item ann)
is1) = String -> NonEmpty (Item ann) -> St ann
forall ann. String -> List1 (Item ann) -> St ann
St String
"" (ann -> [DocTree ann] -> Item ann
forall ann. ann -> [DocTree ann] -> Item ann
Item ann
a [] Item ann -> NonEmpty (Item ann) -> NonEmpty (Item ann)
forall a. a -> NonEmpty a -> NonEmpty a
<| String -> NonEmpty (Item ann) -> NonEmpty (Item ann)
pushStr String
s NonEmpty (Item ann)
is1)
      where
        pushStr :: String -> List1 (Item ann) -> List1 (Item ann)
        pushStr :: String -> NonEmpty (Item ann) -> NonEmpty (Item ann)
pushStr String
"" NonEmpty (Item ann)
is1 = NonEmpty (Item ann)
is1
        pushStr String
s (Item ann
a [DocTree ann]
ts :| [Item ann]
is) = ann -> [DocTree ann] -> Item ann
forall ann. ann -> [DocTree ann] -> Item ann
Item ann
a (Text -> DocTree ann
forall ann. Text -> DocTree ann
Text (String -> Text
Text.pack String
s) DocTree ann -> [DocTree ann] -> [DocTree ann]
forall a. a -> [a] -> [a]
: [DocTree ann]
ts) Item ann -> [Item ann] -> NonEmpty (Item ann)
forall a. a -> [a] -> NonEmpty a
:| [Item ann]
is

-- | Render a @'Doc' ann@ to a @'DocTree' ann@ using standard layout parameters.
renderToTree :: forall ann. Null ann => Doc ann -> DocTree ann
renderToTree :: forall ann. Null ann => Doc ann -> DocTree ann
renderToTree = Int -> Fill -> Doc ann -> DocTree ann
forall ann. Null ann => Int -> Fill -> Doc ann -> DocTree ann
renderToTree' Int
100 Fill
1.5

---------------------------------------------------------------------------
-- * Converting 'DocTree' to 'Text' et al.

-- | Generic 'DocTree' linearization.
renderTree' :: forall ann t. Monoid t => (Text -> t) -> (ann -> t -> t) -> DocTree ann -> t
renderTree' :: forall ann t.
Monoid t =>
(Text -> t) -> (ann -> t -> t) -> DocTree ann -> t
renderTree' Text -> t
txt ann -> t -> t
ann = DocTree ann -> t
go
  where
    go :: DocTree ann -> t
    go :: DocTree ann -> t
go = \case
      Node ann
a [DocTree ann]
ts -> ann -> t -> t
ann ann
a (t -> t) -> t -> t
forall a b. (a -> b) -> a -> b
$ (DocTree ann -> t) -> [DocTree ann] -> t
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap DocTree ann -> t
go [DocTree ann]
ts
      Text Text
t    -> Text -> t
txt Text
t

-- Compatibility layer for different versions of package text.

#if MIN_VERSION_text(2,0,2)

#if MIN_VERSION_text(2,1,2)
type Builder = Data.Text.Encoding.StrictTextBuilder
#else
type Builder = Data.Text.Encoding.StrictBuilder
#endif

builderToText :: Builder -> Text
builderToText :: Builder -> Text
builderToText = Builder -> Text
strictBuilderToText

textToBuilder :: Text -> Builder
textToBuilder :: Text -> Builder
textToBuilder = Text -> Builder
textToStrictBuilder

#else

type Builder = Builder.Builder

builderToText :: Builder -> Text
builderToText = TL.toStrict . Builder.toLazyText

textToBuilder :: Text -> Builder
textToBuilder = Builder.fromText

#endif

-- | Linearize a 'DocTree' to 'Text' with the given 'Text'-rendering of the annotations.
treeToText :: (ann -> Text -> Text) -> DocTree ann -> Text
treeToText :: forall ann. (ann -> Text -> Text) -> DocTree ann -> Text
treeToText ann -> Text -> Text
ann
  = Builder -> Text
builderToText
  (Builder -> Text)
-> (DocTree ann -> Builder) -> DocTree ann -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Builder)
-> (ann -> Builder -> Builder) -> DocTree ann -> Builder
forall ann t.
Monoid t =>
(Text -> t) -> (ann -> t -> t) -> DocTree ann -> t
renderTree' Text -> Builder
textToBuilder \ ann
a -> Text -> Builder
textToBuilder (Text -> Builder) -> (Builder -> Text) -> Builder -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ann -> Text -> Text
ann ann
a (Text -> Text) -> (Builder -> Text) -> Builder -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Builder -> Text
builderToText
-- Naive implementation:
-- treeToText = renderTree' id

-- | Linearize a 'DocTree' to 'Text' dropping all annotations.
treeToTextNoAnn :: DocTree ann -> Text
treeToTextNoAnn :: forall ann. DocTree ann -> Text
treeToTextNoAnn = (ann -> Text -> Text) -> DocTree ann -> Text
forall ann. (ann -> Text -> Text) -> DocTree ann -> Text
treeToText ((Text -> Text) -> ann -> Text -> Text
forall a b. a -> b -> a
const Text -> Text
forall a. a -> a
id)

-- ** Linearizing a 'DocTree' to a 'Text' plus a 'RangeMap'.
--
-- Outputs one annotation interval per 'Node',
-- leaving it to the 'RangeMap' to combine annotations correctly.

treeToTextWithAnn :: (Monoid ann, Null ann) => DocTree ann -> (Text, RangeMap ann)
treeToTextWithAnn :: forall ann.
(Monoid ann, Null ann) =>
DocTree ann -> (Text, RangeMap ann)
treeToTextWithAnn = Int -> Lin ann -> (Text, RangeMap ann)
forall ann. Monoid ann => Int -> Lin ann -> (Text, RangeMap ann)
evalLin Int
0 (Lin ann -> (Text, RangeMap ann))
-> (DocTree ann -> Lin ann) -> DocTree ann -> (Text, RangeMap ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> Lin ann)
-> (ann -> Lin ann -> Lin ann) -> DocTree ann -> Lin ann
forall ann t.
Monoid t =>
(Text -> t) -> (ann -> t -> t) -> DocTree ann -> t
renderTree' Text -> Lin ann
forall ann. Monoid ann => Text -> Lin ann
linText ann -> Lin ann -> Lin ann
forall ann. (Monoid ann, Null ann) => ann -> Lin ann -> Lin ann
linNode

-- | Linearizer state.
data LinSt ann = LinSt
  { forall ann. LinSt ann -> Int
linPosition    :: Int
      -- ^ Current position.
  , forall ann. LinSt ann -> Builder
linBuilder     :: Builder
      -- ^ Accumulated text.
  , forall ann. LinSt ann -> RangeMap ann
linRangeMap    :: RangeMap ann
      -- ^ Accumulated annotation information.
  }

-- | Linearizer.
--   We need forward function composition because we process nodes left-to-right.
type Lin ann = Fwd (LinSt ann)

-- | Run linearizer with given initial offset.
evalLin :: Monoid ann => Int -> Lin ann -> (Text, RangeMap ann)
evalLin :: forall ann. Monoid ann => Int -> Lin ann -> (Text, RangeMap ann)
evalLin Int
start Lin ann
f =
  case Lin ann
f Lin ann -> LinSt ann -> LinSt ann
forall a. Fwd a -> a -> a
`appFwd` Int -> LinSt ann
forall ann. Monoid ann => Int -> LinSt ann
initLinSt Int
start of
    LinSt Int
_ Builder
b RangeMap ann
m -> (Builder -> Text
builderToText Builder
b, RangeMap ann
m)

-- | Initial linearizer state with configurable offset.
initLinSt :: Monoid ann => Int -> LinSt ann
initLinSt :: forall ann. Monoid ann => Int -> LinSt ann
initLinSt Int
start = Int -> Builder -> RangeMap ann -> LinSt ann
forall ann. Int -> Builder -> RangeMap ann -> LinSt ann
LinSt Int
start Builder
forall a. Monoid a => a
mempty RangeMap ann
forall a. Null a => a
empty

-- | Outputting some text under the currently active annotations.
linText :: Monoid ann => Text -> Lin ann
linText :: forall ann. Monoid ann => Text -> Lin ann
linText Text
t = (LinSt ann -> LinSt ann) -> Fwd (LinSt ann)
forall a. (a -> a) -> Fwd a
Fwd \case
  LinSt Int
start Builder
b RangeMap ann
m -> Int -> Builder -> RangeMap ann -> LinSt ann
forall ann. Int -> Builder -> RangeMap ann -> LinSt ann
LinSt Int
end Builder
b' RangeMap ann
m
    where
      end :: Int
end = Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Text -> Int
Text.length Text
t
      b' :: Builder
b'  = Builder
b Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Text -> Builder
textToBuilder Text
t

-- | Add an annotation to the 'RangeMap'.
linNode :: (Monoid ann, Null ann) => ann -> Lin ann -> Lin ann
linNode :: forall ann. (Monoid ann, Null ann) => ann -> Lin ann -> Lin ann
linNode ann
a Lin ann
f = (LinSt ann -> LinSt ann) -> Lin ann
forall a. (a -> a) -> Fwd a
Fwd \case
  st :: LinSt ann
st@LinSt{ linPosition :: forall ann. LinSt ann -> Int
linPosition = Int
start } -> LinSt ann
st'{ linRangeMap = m' }
    where
     -- Render content first to get the end position.
     st' :: LinSt ann
st'@LinSt{ linPosition :: forall ann. LinSt ann -> Int
linPosition = Int
end, linRangeMap :: forall ann. LinSt ann -> RangeMap ann
linRangeMap = RangeMap ann
m } = Lin ann
f Lin ann -> LinSt ann -> LinSt ann
forall a. Fwd a -> a -> a
`appFwd` LinSt ann
st
     r :: Range
r  = Range{ from :: Int
from = Int
start, to :: Int
to = Int
end }
     -- Insert annotation, leaving it to the RangeMap to combine it with the
     -- existing annotations.
     m' :: RangeMap ann
m' = Bool
-> (RangeMap ann -> RangeMap ann) -> RangeMap ann -> RangeMap ann
forall b a. IsBool b => b -> (a -> a) -> a -> a
applyUnless (ann -> Bool
forall a. Null a => a -> Bool
null ann
a) ((ann -> ann -> ann) -> Range -> ann -> RangeMap ann -> RangeMap ann
forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
RangeMap.insert ann -> ann -> ann
forall a. Semigroup a => a -> a -> a
(<>) Range
r ann
a) RangeMap ann
m

-- ** Alternative linearizer (first implementation).
--
-- This alternative does not need a sophisticated 'RangeMap',
-- it takes care of the annotation composition itself
-- and outputs the final intervals in left-to-right order.
--
-- The drawback is that it produces an annotation interval for each 'Text'
-- leaf of the 'DocTree' rather than preserving continguous intervals
-- stretching over subtrees.
-- As 'RangeMap' does not join adjacent intervals,
-- this leads to a lot of tiny intervals,
-- which increases the communication load between Agda and Emacs.

treeToTextWithAnnA :: Monoid ann => DocTree ann -> (Text, RangeMap ann)
treeToTextWithAnnA :: forall ann. Monoid ann => DocTree ann -> (Text, RangeMap ann)
treeToTextWithAnnA = Int -> LinA ann -> (Text, RangeMap ann)
forall ann. Monoid ann => Int -> LinA ann -> (Text, RangeMap ann)
evalLinA Int
0 (LinA ann -> (Text, RangeMap ann))
-> (DocTree ann -> LinA ann) -> DocTree ann -> (Text, RangeMap ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text -> LinA ann)
-> (ann -> LinA ann -> LinA ann) -> DocTree ann -> LinA ann
forall ann t.
Monoid t =>
(Text -> t) -> (ann -> t -> t) -> DocTree ann -> t
renderTree' Text -> LinA ann
forall ann. Monoid ann => Text -> LinA ann
linAText ann -> LinA ann -> LinA ann
forall ann. Monoid ann => ann -> LinA ann -> LinA ann
linANode

-- | Linearizer state.
data LinASt ann = LinASt
  { forall ann. LinASt ann -> Int
bstPosition    :: Int
      -- ^ Current position.
  , forall ann. LinASt ann -> List1 ann
bstAnnotations :: List1 ann
      -- ^ The top of the stack is the currently active annotation(s).
  , forall ann. LinASt ann -> Builder
bstBuilder     :: Builder
      -- ^ Accumulated text.
  , forall ann. LinASt ann -> RangeMap ann
bstRangeMap    :: RangeMap ann
      -- ^ Accumulated annotation information.
  }

-- | Linearizer.
type LinA ann = Fwd (LinASt ann)

-- | Run linearizer with given initial offset.
evalLinA :: Monoid ann => Int -> LinA ann -> (Text, RangeMap ann)
evalLinA :: forall ann. Monoid ann => Int -> LinA ann -> (Text, RangeMap ann)
evalLinA Int
start LinA ann
f =
  case LinA ann
f LinA ann -> LinASt ann -> LinASt ann
forall a. Fwd a -> a -> a
`appFwd` Int -> LinASt ann
forall ann. Monoid ann => Int -> LinASt ann
initLinASt Int
start of
    LinASt Int
_ List1 ann
_ Builder
b RangeMap ann
m -> (Builder -> Text
builderToText Builder
b, RangeMap ann
m)

-- | Initial linearizer state with configurable offset.
initLinASt :: Monoid ann => Int -> LinASt ann
initLinASt :: forall ann. Monoid ann => Int -> LinASt ann
initLinASt Int
start = Int -> List1 ann -> Builder -> RangeMap ann -> LinASt ann
forall ann.
Int -> List1 ann -> Builder -> RangeMap ann -> LinASt ann
LinASt Int
start (ann -> List1 ann
forall el coll. Singleton el coll => el -> coll
singleton ann
forall a. Monoid a => a
mempty) Builder
forall a. Monoid a => a
mempty RangeMap ann
forall a. Null a => a
empty

-- | Outputting some text under the currently active annotations.
linAText :: Monoid ann => Text -> LinA ann
linAText :: forall ann. Monoid ann => Text -> LinA ann
linAText Text
t = (LinASt ann -> LinASt ann) -> Fwd (LinASt ann)
forall a. (a -> a) -> Fwd a
Fwd \case
  LinASt Int
start as :: List1 ann
as@(ann
a :| [ann]
_) Builder
b RangeMap ann
m -> Int -> List1 ann -> Builder -> RangeMap ann -> LinASt ann
forall ann.
Int -> List1 ann -> Builder -> RangeMap ann -> LinASt ann
LinASt Int
end List1 ann
as Builder
b' RangeMap ann
m'
    where
      end :: Int
end = Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Text -> Int
Text.length Text
t
      b' :: Builder
b'  = Builder
b Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Text -> Builder
textToBuilder Text
t
      m' :: RangeMap ann
m'  = (ann -> ann -> ann) -> Range -> ann -> RangeMap ann -> RangeMap ann
forall a. (a -> a -> a) -> Range -> a -> RangeMap a -> RangeMap a
RangeMap.insert ann -> ann -> ann
forall a. Semigroup a => a -> a -> a
(<>) Range
r ann
a RangeMap ann
m
      r :: Range
r   = Range{ from :: Int
from = Int
start, to :: Int
to = Int
end }

-- | Adding an annotation to the currently active ones.
linANode :: Monoid ann => ann -> LinA ann -> LinA ann
linANode :: forall ann. Monoid ann => ann -> LinA ann -> LinA ann
linANode ann
a LinA ann
f = (LinASt ann -> LinASt ann) -> LinA ann
forall a. (a -> a) -> Fwd a
Fwd \case
  st :: LinASt ann
st@LinASt{ bstAnnotations :: forall ann. LinASt ann -> List1 ann
bstAnnotations = as :: List1 ann
as@(ann
a' :| [ann]
_) } ->
    LinA ann
f LinA ann -> LinASt ann -> LinASt ann
forall a. Fwd a -> a -> a
`appFwd` LinASt ann
st{ bstAnnotations = (a <> a') <| as }