The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Hugo,

looking at argument scopes, I don't see how a static adjustment of the parser 
table could work. Cause of argument scopes also syntax which is not visible 
can be used.

Think of the ==> operator defined in Morphisms.v. The signature_scope is not 
visible by default, but since Proper sets its argument scope to 
signature_scope, the ==> operator can be used anyway in the argument to 
Proper. If the parser is restricted to visible syntax, this wouldn't work 
anymore.

I guess what would be needed is a parser using a table with context sensitive 
conditions on each transition in the state table. So if something like

Proper (someequiv ==> someequiv ==> someequiv) someop

is parsed, the parser state transitions belonging to signature_scope are 
enabled for the first argument of Proper, otherwise not. Not sure how 
feasible this would be in a bottom up parser. I guess (from observable 
behavior) what happens right now is that first a parse according the syntax 
defined by all scopes is done resulting in a parse tree and then in a second 
pass the scope resolution is done.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928