[Agda-dev] 2.4.4 roadmap

[Nils Anders Danielsson]

On 2015-10-08 09:45, Andreas Abel wrote:
> The change in the operator parser that breaks any Agda development
> should not be released yet, imho. I am not convinced of its merits
> compared to the breakage it causes.

Default fixities were recently reintroduced by Andrea and Ulf, so things
should break less badly.

> I am not happy with how situations like TERM INFIX PREFIX TERM are
> handled without fixity declarations.

Before we handled this kind of code more or less by accident. In fact,
we also allowed code of the form PREFIX TERM INFIX TERM, and PREFIX TERM
POSTFIX, which I think you and I agree should be rejected.

I looked at an operator-heavy Agda development that can be found online,
and noted why parsing failed. I could find four different reasons:

(1) The default precedence of syntax declarations has changed from -666
     to 20.

(2) An operator was in scope with multiple, inconsistent fixities (and
     not disambiguated by the context).

(3) Code of the form TERM INFIX TERM INFIX TERM, PREFIX TERM INFIX TERM
     or TERM INFIX TERM POSTFIX (with matching precedences).

(4) Code of the form TERM INFIX PREFIX TERM or TERM POSTFIX INFIX TERM
     (with matching precedences).

I think code falling under (2) and (3) should be rejected, and I don't
think we should have multiple default fixities.

The only remaining case is (4). In some cases I could fix both (3) and
(4) at the same time, by introducing a fixity declaration. The
number of remaining cases was small. If people have to update their code
anyway, due to (1)-(3), then the additional cost of (4) might be
negligible.

As we have discussed before it is probably possible to handle (4).
However, this would make the grammar more complicated, so I would prefer
not to do this.

> I am for postponing the release of the new operator parsing.  Sections
> depend on it, but are they already stable?

I'm using sections frequently, and don't currently see a need for
changing anything.

> (There are issues with bloated error messages.)

I tried to fix this during the last Agda meeting. Is this still an
issue?

-- 
/NAD