Grammar adjustments to correct and distinguish between type names and type expressions, and to be explicit about C type grammar

[davidcok]

No description provided.

[vprevosto]

See question about binder grammar rule.

[davidcok]

In C declarations, the * (and any [] ) are part of the variable-ident, as is the case in the binder grammar. So the original grammar was ambiguous, as the * could be part of the type-expr or the variable-ident There are situations in which a type-expr with * etc. and without a variable name are needed, such as in cast expressions. C grammar calls these abstract declarators. However, the grammar for a parameter is type-expr id, which permits (and requires) the non-C declaration style int[] a . So unless the intention is to encourage the non-C styule of declaration, the grammar for parameter needs to change as well. I'm going to be reviewing all of these declaration grammar elements this weekend (in Brittany I hope). Your comments today would be welcome.

…

On Tue, Jul 23, 2019 at 5:19 PM Virgile Prevosto ***@***.***> wrote: ***@***.**** requested changes on this pull request. See question about binder grammar rule. ------------------------------ In binders.tex <#62 (comment)>: > @@ -1,12 +1,14 @@ \begin{syntax} binders ::= binder (, binder)* ; \ - binder ::= type-expr variable-ident; + binder ::= type-name variable-ident; I don't understand this change. As far as I can tell, this would prevent writing something like assert list_positive: \forall list* p; reachable(root, p) ==> p->content > 0; unless we have an explicit typedef for list *. — You are receiving this because you were assigned. Reply to this email directly, view it on GitHub <#62?email_source=notifications&email_token=ABITDQEDSSXOW6OQZVRW2ZTQA4ORVA5CNFSM4H4NADR2YY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOB7JP2FA#pullrequestreview-265485588>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABITDQEXQ7ERALBSXMIQN3LQA4ORVANCNFSM4H4NADRQ> .

[vprevosto]

OK modulo my point on array of unspecified size.

Moreover, I just discovered that there's probably some work to do on ghost declarators (so as to allow taking a pointer over a ghost integer, or have an infinite ghost array), but that will be the object of another PR.