TestTacletEquality ignores semantic switches

[WolframPfeifer]

Description

While working on #3353, I noticed that changes inside of semantic switches in taclets are ignored.

For example, consider the following taclet:

    assignmentMultiplicationInt {
        \find(\modality{#normalassign}{..
                    #loc = #seCharByteShortInt0 * #seCharByteShortInt1;
                ...}\endmodality (post))
        (intRules:arithmeticSemanticsCheckingOF) {
            "Overflow check":
                \add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1)))
        };
        \replacewith({#loc := javaMulInt(#seCharByteShortInt0, #seCharByteShortInt1)}
            \modality{#normalassign}{.. ...}\endmodality (post))
        \heuristics(executeIntegerAssignment)
        \displayname "multiplication"
    };

Compare the corresponding entry in the taclets.old.txt:

== assignmentMultiplicationInt (multiplication) =========================================
assignmentMultiplicationInt {
\find(#normalassign ((modal operator))|{{ ..
  #loc = #seCharByteShortInt0 * #seCharByteShortInt1;
... }}| (post))
\replacewith(update-application(elem-update(#loc (program Variable))(javaMulInt(#seCharByteShortInt0,#seCharByteShortInt1)),#normalassign(post))) 
\heuristics(executeIntegerAssignment)
Choices: programRules:Java}

Note that the part with the semantics switch

        (intRules:arithmeticSemanticsCheckingOF) {
            "Overflow check":
                \add(==> inInt(mul(#seCharByteShortInt0, #seCharByteShortInt1)))
        };

does not occur at all. Thus, changes here are not correctly detected.

Reproducible

always

Steps to reproduce

1. Change something inside the semantics switch of the taclet mentioned above.
2. Generate a new oracle file "taclets.new.txt" by running the method TestTacletEquality::createNewOracle and rename it to taclets.old.txt.

The file is identical to the old version, instead of correctly reflecting the changed taclet.

[mattulbrich]

Does this break/concern the taclet definitions used in KeY or is perhaps the printing to taclets.new.txt etc. broken?

[WolframPfeifer]

Does this break/concern the taclet definitions used in KeY or is perhaps the printing to taclets.new.txt etc. broken?

The printing is broken. However, at the moment I do not know how to fix this. It seems that everything inside the by choice/taclet option switch is ignored by the toString() method of Taclet (and its subclasses).

I think there is another potential problem with the test case: Changes in the types of schema variables are not detected (their declarations are not included in the textual representation).

[unp1]

The printing is broken. However, at the moment I do not know how to fix this. It seems that everything inside the by choice/taclet option switch is ignored by the toString() method of Taclet (and its subclasses).

I think the printing would need to use the corresponding TacletBuilder class. The Taclet instance itself contains only the activated goals.

[wadoon]

In my renovation, I delayed evaluating the Taclet activation options at the latest point. Previously, the Taclet parsing was conditional, which resulted in unnoticed erroneous Taclets, as nobody activated a certain option combination.

It would see some benefits to unifying the evaluation of conditions for Taclets and goal templates in the same time point.

Maybe we can overcome, KeY's bad behavior, that changing activate choice options requires a reload.