The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

> That is, there should be some textual way to just express
> what the hierarchy is intended to be instead of arbitrarily assigning
> integers to various levels. If you then wanted to insert a new
> notation between two others, you would just say "this notation is
> supposed to have higher precedence than notation X but
> lower precedence than notation Y"

Dypgen, a GLR parser generator written in OCaml, supports such style.
You can define abstract priorities as symbols and provide a precedence
relation between them. Each rule can then be annotated with the
priority of the terminals and of the whole production.

http://dypgen.free.fr/ (Documentation/Manual, section 3.1)


%relations patom < pprod <psum

expr:
| INT { $1 } patom
| LPAREN expr RPAREN { $2 } patom
| expr(<=psum) PLUS expr(<psum) { $1 + $3 } psum
| expr(<=pprod) TIMES expr(<pprod)  { $1 * $3 } pprod

On Sun, Nov 10, 2013 at 9:31 PM, Perry E. Metzger 
<perry AT piermont.com>
 wrote:
> On Sat, 9 Nov 2013 23:53:55 -0500 Jason Gross 
> <jasongross9 AT gmail.com>
> wrote:
>> Is there a good explanation somewhere of the level requirements for
>> notations to factor properly?  For example, what level do I have
>> can I substitute in for "L" in the following to make the code
>> type-check?
>>
>> Delimit Scope foo_scope with foo.
>> Notation "x , y" := (prod x y) (at level L, no associativity) :
>> foo_scope. Check (_, _). (* should be pair *)
>> Local Open Scope foo_scope.
>> Check _, _. (* should be prod *)
>>
>> I've tried L = 200, and then the second check fails.  I've tried L
>> = 199, and then the first check fails.  Is there any way to make
>> this work?
>
> Not an answer to your question (unfortunately I have none), but a
> side comment.
>
> The idea of expressing the precedence of operators and notations by
> integers, although very simple, strikes me as a not very
> expressive and especially not human-friendly way to do things.
>
> In fact, the precedence of various notations forms a DAG of sorts,
> and it seems to me that it would be better to say "operator B should
> be higher precedence than A but below C" through some explicit
> notation.
>
> That is, there should be some textual way to just express
> what the hierarchy is intended to be instead of arbitrarily assigning
> integers to various levels. If you then wanted to insert a new
> notation between two others, you would just say "this notation is
> supposed to have higher precedence than notation X but
> lower precedence than notation Y" or "this notation should have
> identical precedence to this other notation".
>
> Integers are simple, of course, but any assignment of levels to
> integers is completely arbitrary and inexpressive (we don't mean to
> say that "+" is at integer X, we mean to say it binds less tightly
> than "*" but exactly as tightly as "-"), and bad in that we may run
> out of integers between two operators so we're forced to pick large
> numbers to express precedences, and these large numbers are not very
> readable either.
>
> A very similar problem shows up in Unix init scripts. System V chose
> to express the ordering of initialization scripts by integers, which
> makes it difficult to understand, say, that X comes before Y because Y
> depends on X. In NetBSD, some colleagues of mine and I created a
> system where init scripts explicitly described their dependencies
> instead, which made everything far more readable. People seemed to
> greatly prefer the new mechanism over integers, and it was quickly
> adopted by other BSD Unix variants.
>
> Perry
> --
> Perry E. Metzger                
> perry AT piermont.com