In SANY, what is the APSubstInNode AST node used for?

[Andrew Helwer]

Here is the Java class in question, which is mirrored in the XML export format. I have run the exporter over every spec I can find and as far as I can tell, APSubstInNode is not used in any of them. Is this a zombie language feature or just an obscure one?

Andrew

[Andrew Helwer]

I figured this out. The clue was from the SubstInNode, which SANY uses to wrap expressions from modules imported using INSTANCE/WITH with substitutions, so the substitutions are lazily applied instead of directly written. As the name suggests then, APSubstInNode is when the same thing happens to an ASSUME/PROVE block. I don't know why the substitution isn't just distributed over ASSUME/PROVE to affect the expressions within, but whatever; this spec will produce an XML export containing an APSubstInNode instance at the M!ap usage point:

---- MODULE Test ----
---- MODULE Inner ----
CONSTANT C
THEOREM ap == ASSUME C PROVE C
====
M == INSTANCE Inner WITH C <- TRUE
THEOREM M!ap
====

This does not appear in the tlaplus/examples, nor any other TLA+ spec floating around that I can find, so it's a pretty obscure feature that is essentially never exercised. Possibly some bugs lurking within.

Andrew Helwer