Nils Anders Danielsson

Consider the following code: ```haskell {-# LANGUAGE OverloadedStrings #-} module Test where import Text.Blaze.Html5 as H import Text.Blaze.Html5.Attributes as A import Text.Blaze.Html.Renderer.Pretty example = putStr $ renderHtml $ docTypeHtml $...

The "Pretty" renderer generates incorrect output

1

Consider the following code: ```haskell {-# LANGUAGE OverloadedStrings #-} module Test where import Text.Blaze.Html5 as H import Text.Blaze.Html5.Attributes as A import Text.Blaze.Html.Renderer.Pretty example = putStr $ renderHtml $ docTypeHtml $...

The following code triggers an internal error in Beluga f65d501160913a10f4b749c620711f0678c58c06: ``` LF empty : type = ; schema ctx = empty; LF t : type = | c : t...

The following code triggers an internal error in Beluga f65d501160913a10f4b749c620711f0678c58c06: ``` LF term : type = | lam : (term → term) → term ; LF pred : (term →...

Possibly quadratic behaviour

12

I grepped for `\+\+ \[` and found several pieces of code that can perhaps lead to quadratic behaviour (I ignored code under `Agda.Auto`): https://github.com/agda/agda/blob/3044510c8966a1876951e807f1393bbc3b5e6169/src/full/Agda/Compiler/MAlonzo/Compiler.hs#L150 https://github.com/agda/agda/blob/3044510c8966a1876951e807f1393bbc3b5e6169/src/full/Agda/Interaction/Options/Base.hs#L782 https://github.com/agda/agda/blob/3044510c8966a1876951e807f1393bbc3b5e6169/src/full/Agda/Syntax/Abstract/Views.hs#L49 https://github.com/agda/agda/blob/3044510c8966a1876951e807f1393bbc3b5e6169/src/full/Agda/Syntax/Concrete.hs#L621 https://github.com/agda/agda/blob/3044510c8966a1876951e807f1393bbc3b5e6169/src/full/Agda/Syntax/Concrete/Operators.hs#L864 https://github.com/agda/agda/blob/3044510c8966a1876951e807f1393bbc3b5e6169/src/full/Agda/Syntax/Parser/Parser.y#L579 https://github.com/agda/agda/blob/3044510c8966a1876951e807f1393bbc3b5e6169/src/full/Agda/Syntax/Parser/Parser.y#L1348...

Glued evaluation

5

I think it makes sense to try out the [glued evaluation](https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/README.md#glued-evaluation) that @AndrasKovacs uses in smalltt (see also his discussion of [paired values](https://github.com/AndrasKovacs/smalltt/blob/989b020309686e04374f1ab7844f468386d2eb2f/README.md#paired-values)). This kind of glued evaluation could lead...

Inconsistent treatment of redeclarations of names

1

Currently the following code is allowed: ```agda module _ where module M where import Agda.Primitive as M import Agda.Builtin.Nat as M ``` However, the following code is rejected: ```agda module...

Changes related to the HTML backend

4

I may have fixed #2735 and #4653. However, I added new components to the state (`stPreAccess`) and environment (`envAccess`) instead of reusing the scope, along with possibly duplicated logic (which...

Links to comments rather than code

2

When linking to some piece of code (rendered by the HTML backend) I would often prefer to link to the comment preceding a definition, rather than the definition itself. However,...

Link to symbolic identifiers

2

In order to make it easier to discover the symbolic identifiers (#2604) I think the HTML backend should generate links to them (when available), rather than to the numeric identifiers....