Fix pretty printer: write annotations correctly and extend the standard modules

[konnov]

This PR fixes two annoying bugs in the pretty writer:

• closes [BUG] Printing incorrect annotation of a variable declaration #633: the annotations of VARIABLES and CONSTANTS are printed in the right positions. This required a bit of refactoring.
• closes [FEATURE] PrettyWriter should extend the standard modules #137: pretty writer adds in the preambule EXTENDS Integers, Sequences, FiniteSets, Apalache, TLC.

Having that we can now feed the results of TLA+ passes back to the TLA+ parser. Two issues remain:

• [FEATURE] Preprocessed TLA+ files should have the same name as the module names #785: SANY requires that the filename is exactly as the module name. This is annoying, but it can be done.
• [FEATURE] Rename variables with $ when expoting modules to files #574: replace $ with something else.

The workflow tasks:

• Tests added for any new code
• Ran make fmt-fix (or had formatting run automatically on all files edited)
• Documentation added for any new functionality
• Entry added to UNRELEASED.md for any new functionality