Disallow periods in message labels

[jjcnn]

We currently allow message labels with periods in them, e.g. { mynamespace.myname : Uint32 0 ; ...}. This makes no sense, since transition parameters cannot have periods in them, so the message will only work if it is sent to a user address, in which case the message field is unnecessary.

The problem are the following productions in ScillaParser.mly:

sid :
| name = ID { ParserName.parse_simple_name name }
| name = SPID { ParserName.parse_simple_name name }
| ns = CID; PERIOD; name = ID { ParserName.parse_qualified_name ns name }
...
msg_entry :
| i = sid; COLON;  l = lit { i, MLit l }
| i = sid; COLON;  v = sid  { i,  MVar (ParserIdentifier.mk_id v (toLoc $startpos(v))) }

This should be changed to something like

sid_no_period :
| name = ID { ParserName.parse_simple_name name }
| name = SPID { ParserName.parse_simple_name name }

sid :
| name = sid_no_period { name }
| ns = CID; PERIOD; name = ID { ParserName.parse_qualified_name ns name }
...
msg_entry :
| i = sid_no_period; COLON;  l = lit { i, MLit l }
| i = sid_no_period; COLON;  v = sid  { i,  MVar (ParserIdentifier.mk_id v (toLoc $startpos(v))) }

The change is not backward compatible because it turns some programs that were hitherto syntactically legal into syntactically illegal programs. Adding a warning for version 0 is not out of the question, though.

[jjcnn]

This problem will almost certainly be solved if we change the abstract syntax of messages from

    | Message of (string * payload) list

to

    | Message of (ER.rep SIdentifier.t * payload) list

and then fix all the resulting type errors.

The reason this will work is that the disambiguator will be changed to call name_def_as_simple_global on the identifier (similar to what it does for transition parameters), and this will disallow qualified names as message fields.