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