The highlighting code should be optimised

[nad]

Elsewhere I wrote the following:

[T]he code that finds the overlapping part could be slow if it is used incorrectly:

agda/src/full/Agda/Interaction/Highlighting/Precise.hs

Lines 451 to 468 in c880f86

	-- | @splitAtC p f@ splits the compressed file @f@ into @(f1, f2)@,
	-- where all the positions in @f1@ are @< p@, and all the positions
	-- in @f2@ are @>= p@.
	splitAtC :: Int -> CompressedFile ->
	(CompressedFile, CompressedFile)
	splitAtC p f = (CompressedFile f1, CompressedFile f2)
	where
	(f1, f2) = split $ ranges f
	split [] = ([], [])
	split (rx@(r,x) : f)
	| p <= from r = ([], rx:f)
	| to r <= p = (rx:f1, f2)
	| otherwise = ([ (toP, x) ], (fromP, x) : f)
	where (f1, f2) = split f
	toP = Range { from = from r, to = p }
	fromP = Range { from = p, to = to r }

However, performance should be OK if we always remove the first part. (If necessary one could presumably optimise the code by using a different data structure.)

The splitC function is called from generateAndPrintSyntaxInfo:

agda/src/full/Agda/Interaction/Highlighting/Generate.hs

Lines 163 to 164 in aea2c53

	(prevTokens, (curTokens, postTokens)) <-
	second (splitAtC to) . splitAtC from <$> useTC stTokens

I added code that counted the length of prevTokens, and this indicates that the worst-case time complexity is at least quadratic in the size of the input file. For instance, consider the following code:

_ : Set₁
_ = Set

_ : Set₁
_ = Set

_ : Set₁
_ = Set

_ : Set₁
_ = Set

_ : Set₁
_ = Set

_ : Set₁
_ = Set

For this code we get the following list of lengths: [0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 0]. For "real" code the numbers can exceed 1000.

I suggest that we define CompressedFile using a data structure that allows us to implement splitC efficiently. One option might be to use a map with Ranges as keys, along with the function splitLookup.

[nad]

Perhaps the new representation can also be used for File, in which case CompressedFile could be removed.

[andreasabel]

5 years ago Guilhem Moulin was working on this, but this wasn't merged. Maybe Guilhem still has the patches. They were on a separate repo.
But if you are fixing this now, @nad, there may be no need to look for the old solution.

I had also looked around for better representations. There are some libraries for interval trees on hackage, but I didn't find one back than that implemented what I wanted.

[nad]

I've implemented some different data structures and run some benchmarks (make std-lib-test). Some observations and comments:

• I made the changes and ran the benchmarks on top of (roughly) commit f86f704 plus the change in commit 92c6f64.
• Times vary quite a lot from run to run.
• Quite a bit of the time spent on computing and serialising highlighting data is not attributed to highlighting when -vprofile:7 is used. I turned off highlighting by editing the code, and limited benchmarking suggests that, before my changes, computation and serialisation of highlighting data accounts for about 4-11% of the time.
• Given the lack of reliability of the benchmarks I am not entirely certain that the new implementation is faster than the previous one for the standard library.
• The problem I mentioned in the OP does not seem to be very important for the standard library. However, I constructed a file with 8580 occurrences of the following piece of code:

  _ : Set₁
  _ = Set

  That file took about four times longer to type-check without my changes.
• I've left several data structures in the code. (In fact, they are all used.) One data structure is used for the first step, where highlighting is gathered, and another for the second step, where it is modified. Some of the operations used for the second step are only implemented for one data structure (RangeMap), but several data structures can be used for the second operation by changing the type synonym HighlightingInfoBuilder.
• I did not find a Haskell implementation of an interval map type with only non-overlapping ranges and the kinds of operations I was looking for, so I implemented my own (RangeMap) using Data.Map.Strict.
• RangeMap could presumably be optimised further, but recompiling Agda and running benchmarks takes a lot of time.
• It might make sense to move some code to one or more modules under Agda.Utils.

[andreasabel]

Excellent!

* It might make sense to move some code to one or more modules under `Agda.Utils`.

Yes, I think it is good to separate the data structure (RangeMap) from its application (map to Aspects).

Please open a PR so we can have a structured discussion with the conveniences offered by the PR functionality.

[nad]

Another comment: The append function (<>) is not associative for Aspects. I think this is the reason for some changes to the highlighting behaviour. @andreasabel, you made append non-associative (66a82e6). I'm not convinced that this is a good idea.

[nad]

I think this is the reason for some changes to the highlighting behaviour.

No, this was due to a mistake I made.

[nad]

I opened a separate issue related to how append is not associative (#5347).

The code passes all the tests now. It took me a few iterations to get the code to work for old versions of GHC. I also changed the implementation. Now the conversion from HighlightingInfoBuilder to HighlightingInfo no longer goes via PositionMap. (The difference in performance seems to be small for the standard library.)

I assume that it is possible to create a more efficient implementation of RangeMap by not reusing the implementation of Data.Map.Strict, but instead having a dedicated tree type with direct support for ranges. For instance, even in the case of no overlap the current implementation of insert uses four tree operations (unless the range is empty), which I guess translates to four tree traversals. It should be possible to traverse the tree just a single time.