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

[Younes]

---- MODULE Inner ----
CONSTANT C

THEOREM ep == C
====

---- MODULE Test ----

M == INSTANCE Inner WITH C <- TRUE

THEOREM M!ep
====

I think a broader case is an instantiated theorem with a plain expression body, like the above. That still produces APSubstInNode, even though the theorem body is not ASSUME/PROVE.

[Andrew Helwer]

Ah that is a good spot, I will have to update the XML Exporter documentation. Thanks!

Andrew

--
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/defbaba5-38df-4e27-826d-0c5a007b3f1dn%40googlegroups.com.