Support module semantics

[will62794]

For the use cases I envision, I was not planning to implement full blown semantics of modules and module imports e.g. EXTENDS, etc. For example, for now I'm just considering operators from the standard modules to be globally available at all times, even without being explicitly imported. This behavior could be re-considered in the future, though, if necessary.

[will62794]

See module notes: http://lamport.azurewebsites.net/tla/newmodule.html.

[will62794]

Preliminary implementation in 6c12345, starting with limited support of EXTENDS based imports.

Handling INSTANCE based imports is a remaining task. Will also need to handle LOCAL INSTANCE semantics.

[lemmy]

Can the CommunityModules be added to the default search path? The root modules of both the CCF Consistency spec and the Azure CosmosDB spec extend them.

[lemmy]

Confirmed that the below doesn't work for CCF's consistency spec because resolving the CommunityModule's Functions and Folds from the CCF repo obviously results in a 404.

tla-web/js/eval.js

Lines 24 to 30 in aeaf642

	// https://github.com/tlaplus/CommunityModules/blob/master/modules
	const TLA_COMMUNITY_MODULES = [
	"SequencesExt",
	"FiniteSetsExt"
	]
	const TLA_COMMUNITY_MODULES_BASE_URL = "https://raw.githubusercontent.com/tlaplus/CommunityModules/master/modules";

tla-web/js/eval.js

Lines 1290 to 1297 in aeaf642

	// Look up CommunityModule imports from hard-coded repo.
	// TODO: This will likely not work properly unitl we handle LOCAL INSTANCE
	// semantics correctly for modules.
	if (TLA_COMMUNITY_MODULES.includes(modName)) {
	return fetch(`${TLA_COMMUNITY_MODULES_BASE_URL}/${modName}.tla`).then(response => response.text());
	}
	return fetch(`${baseSpecPath}/${modName}.tla`).then(response => response.text());

[will62794]

See 538d398.