Jason Gross (Sep 11 2021 at 00:36): Jason Gross (Sep 11 2021 at 00:36):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 ?)
Guillaume Melquiond (Sep 11 2021 at 03:07):This does not make sense to me. If both + and ^ 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?
Enrico Tassi (Sep 11 2021 at 06:22):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?
Enrico Tassi (Sep 11 2021 at 06:23):Especially with custom entries shoul be able to start afresh
Guillaume Melquiond (Sep 11 2021 at 06:28):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.
Paolo Giarrusso (Sep 12 2021 at 08:02):Indeed the Agda parser can reject expressions as ambiguous, so it’d reject a ^ b + c and you’d need parentheses.
Hugo Herbelin (Sep 13 2021 at 15:24):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.
Paolo Giarrusso (Sep 14 2021 at 14:08):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.
Jason Gross (Sep 16 2021 at 16:06):The use case is mechanically porting an Agda project to Coq.
Paolo Giarrusso (Sep 16 2021 at 18:45):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.
Paolo Giarrusso (Sep 16 2021 at 18:48):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.
Paolo Giarrusso (Sep 16 2021 at 18:52):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: Oct 12 2024 at 12:01 UTC