TLAPM parser does not accept `MODULE` references in several places

[ahelwer]

Quoting from TLA Version 2: A Preliminary Guide [pdf], page 20:

The parser also allows the following two kinds of “facts” in a use or hide statement. However, they are not supported by TLAPS and are likely to be removed from the language:

• MODULE Name, indicating that all known facts obtained from the module Name are to be added or removed from the set of usable facts. The module name must appear in an extends or instance statement or else be the name of the current module.

And indeed TLAPM does not accept this syntax (although SANY does):

---- MODULE Test ----
USE x, MODULE M, 1 + 3
HIDE DEFS MODULE M, -., *, ^+
USE x, MODULE M DEF MODULE M, x
====

Though this is not discussed explicitly in the TLA+ V2 document, these "module references" are accepted in another place by SANY and the extant formal TLA+ grammar, which makes sense because they share parsing logic with use-or-hide: PROOF BY statements:

---- MODULE Test ----
LEMMA TRUE
PROOF BY ONLY
  MODULE Naturals,
  MODULE Integers
  DEFS
    MODULE Reals,
    MODULE Sequences
====

So the thing to do here is decide at the standard level whether these statements should actually be allowed in the language.

Ref #159

[muenchnerkindl]

Thanks for reporting this. IMHO, it would indeed be better to remove this syntax from the language, as well as the similar "BY MODULE" construct. These constructs look like a maintainer's headache because changes to a module could cause proof failures elsewhere that are hard to understand. Mild reformulations of facts and even additions of new theorems can confuse the provers to the point that existing proofs may fail. Instead, appealing to specific facts from a module indicates what is needed for a proof step to go through. Expanding all definitions contained in a module breaks the abstraction barrier: usually, one uses definitions to prove facts about operators and then uses those theorems, forgetting the actual definition.