Hugo Herbelin (Jul 23 2020 at 10:39): Hugo Herbelin (Jul 23 2020 at 10:39):@Pierre-Marie Pédrot : I'm experimenting a "small" change in grammar.ml which is to uncomment the famous match strm with parser [] line in start_parser_of_levels so that camlp5 complies (more) with what it is expected to do. As a result, we have to make explicit a couple of RIGHTA in rules of the form foo: [ [ "bar"; foo ] ] so that they work as expected (i.e. moving them to foo: [ RIGHTA [ "bar"; foo ] ]).
Now, it happens that some recursive instances of ARGUMENT EXTEND needs sometimes to be associative to the left (as in rewstrategy, for rewrite_strat) and sometimes associative to the right (as in ssrortacs). Would you be ok that I add an extra optional parameter to ARGUMENT EXTEND so as to control this? Currently I experimented with the syntax RIGHT ASSOCIATIVITY but any syntax would be good to me.
Don't hesitate to ask further questions if you want to know more about the implication of my experiment.
Pierre-Marie Pédrot (Jul 23 2020 at 10:54):Yep, it makes sense to control associativity for recursive arguments.
Hugo Herbelin (Jul 23 2020 at 12:40):Actually, rewstrategy is more complex than that (it mixes infix and prefix) and would require levels. So, at the end, only right associativity is needed in practice and we could also decide that the default for ARGUMENT EXTEND is always to be right associative. I'm perplex.
About rewstrategy (which is already ambiguous, e.g. repeat c ; repeat d has two valid interpretations in the grammar), I see two possibilities. Either recursive declarations as in:
ARGUMENT EXTEND rewstrategy0 ... WITH rewstrategy1 ... END
or extensible declarations, like:
ARGUMENT EXTEND rewstrategy0 ... <no rule> END
ARGUMENT EXTEND rewstrategy1 ... <depending on rewstrategy0> END
ARGUMENT EXTEND rewstrategy0 ... <depending on rewstrategy1> END
Don't know if you have an opinion.
Enrico Tassi (Jul 23 2020 at 12:53):I'm not sure I fully understand the issue, but the latter proposal would help in SSR. IIRC we have to use the lower level GEXTEND in place of the latter ARGUMENT EXTEND to actually implement recursion (even in very simple cases).
Hugo Herbelin (Jul 23 2020 at 19:13):IIRC we have to use the lower level GEXTEND in place of the latter ARGUMENT EXTEND to actually implement recursion
That's what I was actually wondering.
I'm leaning towards this solution: In tacentries.ml, split argument_extend in two:
Then, we can implement either a mutual ARGUMENT EXTEND bloc, or an extensible ARGUMENT EXTEND.
Hugo Herbelin (Jul 23 2020 at 19:14):I'd be almost ready to do it now, but maybe @Pierre-Marie Pédrot has another idea on how to do it.
Last updated: Apr 20 2024 at 05:01 UTC