@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.
Yep, it makes sense to control associativity for recursive arguments.
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.
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).
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
.
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: Oct 13 2024 at 01:02 UTC