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 HelwerOn Tuesday, December 31, 2024 at 6:33:41 PM UTC-5 wjs...@xxxxxxxxxxx wrote:M2 would import definitionsH1!CCC == 99H1!ExprM3 == 43 + CCCand Main would then import both of these, prefixed asH!H1!CCC == 99H!H1!ExprM3 == 43 + CCCso 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:CCC is also imported into M2 as H1!CCC, so the Main _expression_ should resolve to `43 + H!H1!CCC`.
On Tue, Dec 31, 2024, 11:41 AM William Schultz <will...@xxxxxxxxx> wrote:Consider the following set of modules:---- MODULE M3 ----
EXTENDS Sequences, Naturals
CCC == 99
ExprM3 == 43 + CCC
====---- MODULE M2 ----H1 == INSTANCE M3
====---- MODULE Main ----
EXTENDS NaturalsVARIABLE xH == INSTANCE M2Init == 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 + CCCThis 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.--
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...@xxxxxxxxxxxxxxxx.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/ed20d2bb-76b3-4d7f-bbd8-d5d7a95129a7n%40googlegroups.com.