Module instantiation semantics

[William Schultz]

Consider the following set of modules:

---- MODULE M3 ----
EXTENDS Sequences, Naturals
CCC == 99
ExprM3 == 43 + CCC
====

---- MODULE M2 ----

H1 == INSTANCE M3
====

---- MODULE Main ----
EXTENDS Naturals

VARIABLE x

H == INSTANCE M2

Init == x = H!H1!ExprM3
Next == x' = x
====

Based on my understanding of instantiation semantics (from Chapter 17 of Specifying Systems, "The Meaning of a Module"), the H == INSTANCE M2 definition in the Main module will import into Main all definitions from M2 but prefixed with H!. This will (transitively) include all definitions from M3 prefixed with H1! (i.e. the definitions from M3 will be prefixed by H!H1!). 

So, in Main, the expression H!H1!ExprM3 would then refer, syntactically, to the expression 

43 + CCC

This seems problematic, though, since CCC is not actually a definition that appears in the context of Main by the basic instantiation rules. 

Is there some detail about instantiation semantics I am missing here? Intuitively, it seems as if CCC in the case above should in some sense be evaluated "in the context of" M3 (i.e. where CCC is a well defined expression), but I am trying to reconcile this with the basic instantiation rules as I understand them. 

[Hillel Wayne]

CCC is also imported into M2 as H1!CCC, so the Main expression should resolve to `43 + H!H1!CCC`.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ed20d2bb-76b3-4d7f-bbd8-d5d7a95129a7n%40googlegroups.com.

[wjs...@cornell.edu]

M2 would import definitions

H1!CCC == 99

H1!ExprM3 == 43 + CCC

and Main would then import both of these, prefixed as

H!H1!CCC == 99

H!H1!ExprM3 == 43 + CCC

so evaluation of H!H1!ExprM3 is sensible in Main, but its naive syntactic definition refers to CCC, which is not defined in Main. 

Perhaps one way to view this correctly, based on rules outlined in 17.5.3 of Specifying Systems, is that when ExprM3 is defined in its original module, its "current context" (roughly, the set of declarations + definitions defined up to that point) contains the definition CCC. And, this "current context" at the time of definition would be maintained across module imports. So, upon evaluation of H!H1!ExprM3 in Main, its context still contains direct definition of CCC. In other words, a definition is evaluated in a specific context, which is "captured" at the time of its original definition.

Alternatively, I suppose this may be addressed by always appropriately renaming any definitions that were imported via an instantiated module e.g. in the case above, when M2 instantiates H1, importing all definitions from M3, it should also rename all references to definitions in M3 with an H1! prefix.

[Andrew Helwer]

Since semantic analysis & symbol resolution starts at the leaf modules and completes at the main entry point, by the time H!H1!ExprM3 is resolved CCC will already have been resolved to the CCC definition in module M3 (presumably stored as some kind of "refers to" metadata associated with the identifier, or whatever other system you want to use). Or maybe I'm thinking about this too mechanically? I could see this being an issue if you resolve definitions by expanding them inline, macro-style.

Andrew Helwer

[Andrew Helwer]

Another case to consider is with the LOCAL keyword. Like:

---- MODULE Root ----

EXTENDS Naturals, Leaf

VARIABLE x

Init == x = def

Next == x' = x

====

---- MODULE Leaf ----

LOCAL def2 == 0

def == def2

====

A straightforward reading of the import semantics would leave def pointing to a nonexistent symbol within the context of the Root module.

Andrew Helwer

[William Schultz]

M2 would import definitions

H1!CCC == 99

H1!ExprM3 == 43 + CCC

and Main would then import both of these, prefixed as

H!H1!CCC == 99

H!H1!ExprM3 == 43 + CCC

so evaluation of H!H1!ExprM3 is sensible in Main, but its naive syntactic definition refers to CCC, which is not defined in Main. 

Perhaps one way to view this correctly, based on rules outlined in 17.5.3 of Specifying Systems, is that when ExprM3 is defined in its original module, its "current context" (roughly, the set of declarations + definitions defined up to that point) contains the definition CCC. And, this "current context" at the time of definition would be maintained across module imports. So, upon evaluation of H!H1!ExprM3 in Main, its context still contains direct definition of CCC. In other words, a definition is evaluated in a specific context, which is "captured" at the time of its original definition.

Alternatively, I suppose this may be addressed by always appropriately renaming any definitions that were imported via an instantiated module e.g. in the case above, when M2 instantiates H1, importing all definitions from M3, it should also rename all references to definitions in M3 with an H1! prefix.

On Tuesday, December 31, 2024 at 11:48:56 AM UTC-5 Hillel Wayne wrote:

[Andrew Helwer]

One alternative way of thinking about it is that scope/contexts aren’t real, only things referring to other things are real. As I understand it this perspective is fairly popular in the interpreter community although I don’t have anything to really back that up.

Andrew

[Andrew Helwer]

Now that I'm more familiar with how SANY works I might be able to answer this in greater detail. So consider your modules M2 and M3:

---- MODULE M3 ----
EXTENDS Sequences, Naturals
CCC == 99
ExprM3 == 43 + CCC
====

---- MODULE M2 ----

H1 == INSTANCE M3
====

M3 will be processed first; what happens is that all definitions in Sequences, Naturals, and their transitive closure are inlined in M3. So there will be a Nat, +, Seq, etc. copied wholesale into M3. Note that whenever an operator is inlined in this way, its location metadata remains tied to its origin. So the Seq operator will appear as a unit-level definition of the M3 module, but if you look at its location metadata it will still say it's in the Sequences module.

Next up is M2. SANY separates INSTANCE imports that use substitution from those that do not. In this case, M3 is imported without any substitution. This means that SANY takes all definitions in M3 (including those inlined from Sequences, Naturals, etc.) and prepends the string H1! to them then inlines them in M2. This means that there is a real actual definition that looks like H1!CCC == 99 or named H1!+ copied into module M2 where H1 == INSTANCE M3 is. Of course TLA+ does not allow "!" in operator definition names like this, but we are past the point where that is checked and so this "illegal" operator name is fine and functions like any other string for the purpose of name resolution.

Now moving on to Main:

---- MODULE Main ----
EXTENDS Naturals

VARIABLE x

H == INSTANCE M2

Init == x = H!H1!ExprM3
Next == x' = x
====

First off all definitions from the transitive closure of Naturals are inlined in Main. Then we have H == INSTANCE M2, which does not use any substitution. Thus all definitions from M2 are inlined in Main, making a bunch of operator definitions with names like H!H1!+ (existing alongside the regular + operator inlined by EXTENDS Naturals!) and H!H1!CCC. In particular your question asked about how H!H1!ExprM3 is evaluated. The answer is that H!H1!ExprM3 == 43 + CCC is a new operator definition inlined in Main. But then how is CCC resolved? The answer is somewhat unsatisfying. At the time that module M3 was processed, CCC was analyzed and assigned a globally unique identifier (in the AST I'm looking at, number 540). Then ExprM3's body was processed to roughly +(Numeral(43), OpId(540)). And that's exactly how it was inlined all the way up the chain, until H!H1!ExprM3, which was also defined to be +(Numeral(43), OpId(540)). So operator bodies are not rewritten when they are inlined.

You might reasonably ask what's the point of all this inlining if operator GUID references could be used instead. To that I don't have an answer other than maybe it made this whole transitive inlining/scope-checking process a lot less error-prone.

I mentioned that substitutive INSTANCE imports are a whole different beast. Interestingly, SANY does not seem to rewrite substitutive import definitions at all; rather, every reference to a substitutive import definition is wrapped with a list of the substitutions, and it's up to the evaluator to apply those substitutions when evaluating the expression. Possibly somewhat inefficient but in keeping with the general rule that SANY does not rewrite/substitute expressions, only definitions.

Andrew Helwer