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.
On Tuesday, December 31, 2024 at 8:41:37 AM UTC-8 William Schultz 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 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.