TLA+ module support (for completeness)

[fhackett]

Currently, PGo will crash with NotImplementedError if a TLA+ module it's compiling references external definitions.

Anything involving EXTENDS, INSTANCE and a module that is not built-in will cause this problem.

While this does not impact most usage, it would be good to eventually implement the relevant scoping / compilation features.

[minhnhdo]

tracking branch: https://github.com/minhnhdo/pgo/tree/matthew-extends-support

[fhackett]

Good to see work's gotten started; commits make sense so far :)

Some notes I forgot to add originally:

• A non-obvious consequence of these requirements will probably be to implement an error in case of duplicate definitions. This is needed due to the TLA+ module system's solution to the diamond inheritance problem, which relies on uniqueness to make actual sense. TLA+ forbids name shadowing, but PGo doesn't actually care right now. This will probably matter more then loading multiple possibly-conflicting definitions, as with custom modules.
• You can identify definitions by "pointer identity", at least at the parser+scoping stage, and the withDefinition function could be a good place to insert any such logic (give or take some potentially tricky interactions with parser backtracking).
• If you didn't find it already, have a look at the MPCal parser's logic, re: how it extracts relevant TLA+ definitions to consider in-scope for the MPCal block (it does this at its entry point, in the object). This should be more or less adaptable to implementing the module "inclusion" primitives.