Ana de Almeida Borges (Mar 10 2021 at 17:57): Ana de Almeida Borges (Mar 10 2021 at 17:57):As the title says. I thought it might be fixable with appropriate scopes, but apparently not.
Require Import ssrbool.
Check [&& true, true & true]. (* everything is fine *)
Variable (T : Type).
Declare Scope T_scope.
Bind Scope T_scope with T.
Variable (f : T -> T -> T).
Infix "&" := f (at level 60) : T_scope.
Check [&& true, true & true]. (* fails *)
(* Syntax error: ',' or '&' expected after [term level 200] (in [term]). *)
What does work is declaring "&" at level 200, but that doesn't feel like a real solution... Is there a way to use & in such a notation, or should I just give up and pick another symbol?
Michael Soegtrop (Mar 10 2021 at 17:59):Afaik scopes change the interpretation of the parse tree but not the parser. If you declare a notation the parser is changed, regardless what the scope is.
Ana de Almeida Borges (Mar 10 2021 at 19:10):So having a way of interpreting a & b just stops Coq from realizing that it is not even well-typed and looking for a different interpretation that uses more surrounding symbols? Must we always avoid notations that are substrings of existing notations?
Ana de Almeida Borges (Mar 10 2021 at 19:11):That can't be right, at the very least both a < b and a < b < c exist and one is a substring of the other.
Christian Doczkal (Mar 10 2021 at 19:21):If you look at the point where the levels of the two notations are fixed (Coq.Init.Notations) you find:
Reserved Notation "x < y" (at level 70, no associativity).
Reserved Notation "x < y < z" (at level 70, y at next level).
The point here is, that the levels of the first/only < is the same in both notations, allowing the parser to parse both notations depending on what comes after.
Ana de Almeida Borges (Mar 10 2021 at 19:30):So that's why defining "&" at level 200 works, and there is no other workaround?
Christian Doczkal (Mar 10 2021 at 19:36):I don't know what exactly you mean by "it works" for level "200". It still does not seem to parse x & x, it only parses the iterated conjunction.
Ana de Almeida Borges (Mar 10 2021 at 19:38):Oh, you're right, I forgot to check that.
Christian Doczkal (Mar 10 2021 at 19:38):But yes, I would stay away from using an infix &, it's not only used in all the n-ary operators, but also & A is notation for (_ : A) and it occurs again in the notation for sigT: { x : T & T_ x}
Ana de Almeida Borges (Mar 10 2021 at 19:41):Fair enough, but this makes me a bit sad. I don't suppose you have any ideas for a symbol that means conjunction and is not yet being used in a number of notations?
Christian Doczkal (Mar 10 2021 at 19:44):It depends a bit on your editor, emacs+company-coq has has decent support for entering unicode symbols. So you might even be able to take a symbol that gets mapped to exactly the same glyph. Not that I'm really suggesting this, but it could be a possibility.
Christian Doczkal (Mar 10 2021 at 19:44):But yes, Unicode is probably the way to go for one-symbol infix notations.
Ana de Almeida Borges (Mar 10 2021 at 19:46):Haha yeah, I'm a bit allergic to fancy unicode symbols for some reason, but I guess I can't complain of lack of symbols if I refuse to use 75% of them. Thank you for the help!
Christian Doczkal (Mar 10 2021 at 19:48):More like 99,9%, but yes. Of course, this doesn't solve the problem that one still cannot load two libraries together that use the same symbols with different precedence. But that's a topic for another discussion. :grinning:
Ana de Almeida Borges (Mar 10 2021 at 19:53):(I did briefly wonder which number to pick, but I admit I'm surprised and that on second thought I shouldn't be)
Has that discussion been had anywhere that I could read?
Emilio Jesús Gallego Arias (Mar 10 2021 at 20:12):@Ana de Almeida Borges maybe you can do what you using custom entrie
Emilio Jesús Gallego Arias (Mar 10 2021 at 20:13):Indeed scopes are used for resolution after-parsing, so in that sense notations at the parsing level are global and have to shared, however we recently added support for user-defined "entries" [really, non-terminals if you would like to think that way] which allow for you to define a totally different grammar without conflicting with the usual "entry" that represents for example a Coq term [named constr]
Ana de Almeida Borges (Mar 10 2021 at 20:48):Wow, I had no idea this was a thing. Thank you! It certainly looks like it would solve my issue.
Emilio Jesús Gallego Arias (Mar 10 2021 at 21:36):Most welcome! The whole setup is a bit experimental but with the goal to actually cover your use case, so don't hesitate to open issues about things that can be improved
Last updated: Apr 19 2024 at 19:02 UTC