Agda's mixfix supports both left associative and right associative infix notations at the same precedence level. Coq does not. Why is this? (cc @Hugo Herbelin ?)
This does not make sense to me. If both
^ were at the same level, how would you unambiguously parse
a^b+c? At some point, you have to decide that one operator is more associative than the other. Or does Agda force you to put parentheses on such an expression?
I think that he refers to the fact that associativity is associated, by camlp5, not to the operator but to the level. So two unrelated notations in different scopes cannot place at level x two operations that associate differently. IMO it is not a big deal, do you have a relevant use case Jason?
Especially with custom entries shoul be able to start afresh
But what would it mean to have different associativity at the same level? This is not specific to Camlp5. Other parser generators such as Bison and Menhir also forbid you to do so. And for good reason. As I said, this instantly makes the grammar ambiguous.
Indeed the Agda parser can reject expressions as ambiguous, so it’d reject
a ^ b + c and you’d need parentheses.
Rejecting ambiguous expressions at interpretation time rather than parsing time is probably possible. @Arthur Charguéraud has some ideas to overhaul the notation system and maybe this kind of flexibility can be discussed at this time.
As long as you don’t generate exponentially many parse trees; Agda generates them lazily (which might be easier in Haskell). I agree with Enrico on asking for a usecase.
The use case is mechanically porting an Agda project to Coq.
For that, could you support Agda's rational priorities, and split the Agda level into two, one left and one right associative? I haven’t thought long about this, but _it seems that_ the relative precedence cannot matter when porting non-ambiguous Agda sources: if you have left-associative and right-associative operators next to each other without parentheses, the source is ambiguous.
While that change might still touch lots of code, that’s conceptually much easier. While changing the parsing model would be more complex to implement, introduce ambiguity errors that are impossible today, etc.
Even if this doesn’t work, IMHO this usecase alone seems far too weak. Coq (and Coq’s parsing) has more pressing issues. OTOH, if you’re redesigning the parser from scratch, the changes might be much cheaper.
Last updated: Dec 07 2023 at 09:01 UTC