Automatically Generate EQ Taclets

key.core/src/main/java/de/uka/ilkd/key/macros/HeapSimplificationMacro.java

@@ -74,7 +74,7 @@ public String getDescription() {
 
         "allFieldsEq", "subsetSingletonLeft", "subsetSingletonLeftEQ", "subsetSingletonRight",
         "subsetSingletonRightEQ", "subsetUnionLeft", "subsetUnionLeftEQ",
-        "subsetOfIntersectWithItSelfEQ1", "subsetOfIntersectWithItSelfEQ2", "allFieldsSubsetOf",
+        "subsetOfIntersectWithItSelf1EQ", "subsetOfIntersectWithItSelf2EQ", "allFieldsSubsetOf",
         "disjointAllFields", "disjointAllObjects", "disjointInfiniteUnion",
         "disjointInfiniteUnion_2", "intersectAllFieldsFreshLocs", "disjointWithSingleton1",
         "disjointWithSingleton2", "sortsDisjointModuloNull",

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -104,8 +104,8 @@ public Object visitRulesOrAxioms(JavaKeYParser.RulesOrAxiomsContext ctx) {
         }
         ChoiceExpr choices = accept(ctx.choices);
         this.requiredChoices = Objects.requireNonNullElse(choices, ChoiceExpr.TRUE);
-        List<Taclet> seq = mapOf(ctx.taclet());
-        topLevelTaclets.addAll(seq);
+        List<List<Taclet>> seq = this.mapOf(ctx.taclet());
+        topLevelTaclets.addAll(seq.stream().flatMap(Collection::stream).toList());
         disableJavaSchemaMode();
         return null;
     }
@@ -144,7 +144,7 @@ public TacletBuilder<?> visitTriggers(JavaKeYParser.TriggersContext ctx) {
     }
 
     @Override
-    public Taclet visitTaclet(JavaKeYParser.TacletContext ctx) {
+    public List<Taclet> visitTaclet(JavaKeYParser.TacletContext ctx) {
         Sequent assumesSeq = JavaDLSequentKit.getInstance().getEmptySequent();
         ImmutableSet<TacletAnnotation> tacletAnnotations = DefaultImmutableSet.nil();
         if (ctx.LEMMA() != null) {
@@ -178,7 +178,7 @@ public Taclet visitTaclet(JavaKeYParser.TacletContext ctx) {
 
             registerTaclet(ctx, r, doc, origin);
             currentTBuilder.pop();
-            return r;
+            return List.of(r);
         }
 
         // schema var decls
@@ -243,14 +243,174 @@ public Taclet visitTaclet(JavaKeYParser.TacletContext ctx) {
             Taclet r = peekTBuilder().getTaclet();
             String doc = processDocumentation(ctx.doc);
             registerTaclet(ctx, r, doc, origin);
+            List<Taclet> res = new LinkedList<>();
+            res.add(r);
+            if (ctx.modifiers().generateEQ() != null && !ctx.modifiers().generateEQ().isEmpty()) {
+                // Generate EQ taclet
+                if (ctx.modifiers().generateEQ().size() != 1) {
+                    semanticError(ctx.modifiers(),
+                        "A taclet may have at most one \\generateEQ declaration.");
+                }
+                JavaKeYParser.GenerateEQContext generateEQContext =
+                    ctx.modifiers().generateEQ().getFirst();
+                JTerm eqTerm = accept(generateEQContext.term());
+                if (eqTerm == null) {
+                    semanticError(generateEQContext.term(), "failed to build term.");
+                } else {
+                    List<RuleSet> rs = generateEQContext.ruleset().isEmpty() ? null
+                            : mapOf(generateEQContext.ruleset());
+                    var eqTB =
+                        generateEQTaclet(generateEQContext, b, eqTerm,
+                            rs == null ? null : ImmutableList.fromList(rs));
+                    Taclet eqTaclet = eqTB.getTaclet();
+                    res.add(eqTaclet);
+                    currentTBuilder.push(eqTB);
+                    registerTaclet(ctx, eqTaclet, doc, origin);
+                    currentTBuilder.pop();
+                }
+            }
             setSchemaVariables(schemaVariables().parent());
             currentTBuilder.pop();
-            return r;
+            return res;
         } catch (RuntimeException e) {
             throw new BuildingException(ctx, e);
         }
     }
 
+    /// Generate the EQ version of the taclet represented by `tb`.
+    /// @param tb builder of the original taclet
+    /// @param eqTerm the term to look for in the assumes sequent
+    /// @param ruleSets overriding rule sets
+    /// @return a [TacletBuilder] for the EQ taclet
+    private TacletBuilder<? extends Taclet> generateEQTaclet(JavaKeYParser.GenerateEQContext ctx,
+            TacletBuilder<? extends Taclet> tb,
+            JTerm eqTerm, @Nullable ImmutableList<RuleSet> ruleSets) {
+        var fb = tb.copy();
+        var TB = services.getTermBuilder();
+        setSchemaVariables(new Namespace<>(schemaVariables()));
+        // Extend name and display name by "EQ"
+        fb.setName(new Name(fb.getName() + "EQ"));
+        fb.setDisplayName(fb.getTaclet().displayName() + "EQ");
+        // We add the SV "EQ"
+        TermSV eqSV = SchemaVariableFactory.createTermSV(new Name("EQ"), eqTerm.sort());
+        schemaVariables().add(eqSV);
+        JTerm eqSVTerm = TB.var(eqSV);
+        // Replace `eqTerm` by `EQ` in existing `\assumes`
+        var assumesSeq = replace(fb.assumesSequent(), eqTerm, eqSVTerm);
+        // Add `eqTerm = EQ ==>` to `\assumes`
+        assumesSeq = assumesSeq
+                .addFormula(new SequentFormula(TB.equals(eqTerm, eqSVTerm)), true, false).sequent();
+        fb.setAssumesSequent(assumesSeq);
+        if (ruleSets != null)
+            fb.setRuleSets(ruleSets);
+        boolean changed = false;
+        switch (fb) {
+            case AntecTacletBuilder atb -> {
+                Sequent replaced = (Sequent) replace(atb.getFind(), eqTerm, eqSVTerm);
+                changed = !replaced.equals(atb.getFind());
+                atb.setFind(replaced);
+            }
+            case SuccTacletBuilder stb -> {
+                Sequent replaced = (Sequent) replace(stb.getFind(), eqTerm, eqSVTerm);
+                changed = !replaced.equals(stb.getFind());
+                stb.setFind(replaced);
+            }
+            case RewriteTacletBuilder<?> rb -> {
+                JTerm replaced = (JTerm) replace(rb.getFind(), eqTerm, eqSVTerm);
+                changed = !replaced.equals(rb.getFind());
+                rb.setFind(replaced);
+                // Add the default `\sameUpdateLevel`
+                rb.setApplicationRestriction(rb.getTaclet().applicationRestriction()
+                        .combine(ApplicationRestriction.SAME_UPDATE_LEVEL));
+            }
+            default -> {
+            }
+        }
+        if (!changed) {
+            semanticError(ctx,
+                "The term in \\generateEQ was not found in the taclet's \\find part");
+        }
+        ImmutableList<org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate> goalSpecs =
+            ImmutableList.nil();
+        // We need to replace `eqTerm` by `EQ` in the `\find` parts of added rules as well
+        for (var tgt : fb.goalTemplates()) {
+            ChoiceExpr soc = fb.getGoal2Choices().get(tgt);
+            if (tgt.rules() != null && !tgt.rules().isEmpty()) {
+                ImmutableList<Taclet> rules = ImmutableList.nil();
+                for (var r : tgt.rules()) {
+                    if (r instanceof FindTaclet ft) {
+                        TacletBuilder<? extends Taclet> builder = taclet2Builder.get(ft).copy();
+                        Taclet newTaclet = switch (builder) {
+                            case AntecTacletBuilder atb -> {
+                                atb.setFind((Sequent) replace(atb.getFind(), eqTerm, eqSVTerm));
+                                yield atb.getTaclet();
+                            }
+                            case SuccTacletBuilder stb -> {
+                                stb.setFind((Sequent) replace(stb.getFind(), eqTerm, eqSVTerm));
+                                yield stb.getTaclet();
+                            }
+                            case RewriteTacletBuilder<?> rtb -> {
+                                rtb.setFind((JTerm) replace(rtb.getFind(), eqTerm, eqSVTerm));
+                                yield rtb.getTaclet();
+                            }
+                            default -> throw new UnsupportedOperationException();
+                        };
+                        rules = rules.append(newTaclet);
+                        taclet2Builder.put(newTaclet, builder);
+                    } else {
+                        // No `\find` -> keep original
+                        rules = rules.append((Taclet) r);
+                    }
+                }
+                // Update added rules of goal template
+                org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate newGoalSpec =
+                    switch (tgt) {
+                        case AntecSuccTacletGoalTemplate astg ->
+                            new AntecSuccTacletGoalTemplate(astg.sequent(), rules,
+                                astg.replaceWith(), astg.addedProgVars());
+                        case RewriteTacletGoalTemplate rtg -> new RewriteTacletGoalTemplate(
+                            rtg.sequent(), rules, rtg.replaceWith(), rtg.addedProgVars());
+                        default -> tgt;
+                    };
+                goalSpecs = goalSpecs.append(newGoalSpec);
+                if (soc != null) {
+                    fb.getGoal2Choices().remove(tgt);
+                    fb.getGoal2Choices().put((TacletGoalTemplate) newGoalSpec, soc);
+                }
+            } else {
+                // Keep original goal spec
+                goalSpecs = goalSpecs.append(tgt);
+            }
+        }
+        fb.setTacletGoalTemplates(goalSpecs);
+        setSchemaVariables(schemaVariables().parent());
+        return fb;
+    }
+
+    private SyntaxElement replace(SyntaxElement se, JTerm find, JTerm to) {
+        if (se instanceof Sequent seq)
+            return replace(seq, find, to);
+        if (se instanceof JTerm t)
+            return replace(t, find, to);
+        return se;
+    }
+
+    private Sequent replace(Sequent se, JTerm find, JTerm to) {
+        ImmutableList<SequentFormula> ante = ImmutableList.nil();
+        for (var sf : se.antecedent().asList()) {
+            ante = ante.append(new SequentFormula(replace((JTerm) sf.formula(), find, to)));
+        }
+        ImmutableList<SequentFormula> succ = ImmutableList.nil();
+        for (var sf : se.succedent().asList()) {
+            succ = succ.append(new SequentFormula(replace((JTerm) sf.formula(), find, to)));
+        }
+        return JavaDLSequentKit.createSequent(ante, succ);
+    }
+
+    private JTerm replace(JTerm se, JTerm find, JTerm to) {
+        return GenericTermReplacer.replace(se, t -> t.equals(find), (ignored) -> to, services);
+    }
+
     private void registerTaclet(JavaKeYParser.Datatype_declContext ctx, TacletBuilder<?> tb) {
         var taclet = tb.getTaclet();
         taclet2Builder.put(taclet, peekTBuilder());
@@ -863,8 +1023,8 @@ public ImmutableSet<SchemaVariable> visitAddprogvar(JavaKeYParser.AddprogvarCont
 
     @Override
     public ImmutableList<Taclet> visitTacletlist(JavaKeYParser.TacletlistContext ctx) {
-        List<Taclet> taclets = mapOf(ctx.taclet());
-        return ImmutableList.fromList(taclets);
+        List<List<Taclet>> taclets = mapOf(ctx.taclet());
+        return ImmutableList.fromList(taclets.stream().flatMap(Collection::stream).toList());
     }
 
     private @NonNull TacletBuilder<?> createTacletBuilderFor(Object find,
@@ -1077,14 +1237,14 @@ protected JOperatorSV declareSchemaVariable(ParserRuleContext ctx, String name,
         }
 
         if (variables().lookup(v.name()) != null) {
-            semanticError(null, "Schema variables shadows previous declared variable: %s.",
+            semanticError(ctx, "Schema variables shadows previous declared variable: %s.",
                 v.name());
         }
 
         if (schemaVariables().lookup(v.name()) != null) {
             JOperatorSV old = (JOperatorSV) schemaVariables().lookup(v.name());
             if (!old.sort().equals(v.sort())) {
-                semanticError(null,
+                semanticError(ctx,
                     "Schema variables clashes with previous declared schema variable: %s.",
                     v.name());
             }

key.core/src/main/java/de/uka/ilkd/key/rule/SuccTaclet.java

@@ -78,6 +78,4 @@ protected StringBuffer toStringFind(StringBuffer sb) {
             (Sequent) find,
             prefixMap, choices, tacletAnnotations);
     }
-
-
 }

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecTacletBuilder.java

@@ -94,4 +94,33 @@ public AntecTaclet getAntecTaclet() {
             choices, tacletAnnotations);
         return t;
     }
+
+    @Override
+    public AntecTacletBuilder copy() {
+        var rb = new AntecTacletBuilder().setFind((Sequent) getFind());
+        rb.setAnnotations(tacletAnnotations);
+        rb.setApplicationRestriction(applicationRestriction);
+        rb.setAssumesSequent(assumesSeq);
+        rb.setChoices(choices);
+        rb.setDisplayName(attrs.displayName());
+        rb.setName(name);
+        rb.setTacletGoalTemplates(goals);
+        rb.setTrigger(attrs.trigger());
+        rb.setRuleSets(ruleSets);
+        for (var vc : variableConditions) {
+            rb.addVariableCondition(vc);
+        }
+        rb.addVarsNew(varsNew);
+        rb.addVarsNotFreeIn(varsNotFreeIn);
+        for (var vc : varsNewDependingOn) {
+            rb.addVarsNewDependingOn(vc.first(), vc.second());
+        }
+        rb.setFind((Sequent) find);
+        rb.setChoices(choices);
+        if (goal2Choices != null)
+            rb.goal2Choices =
+                (java.util.HashMap<TacletGoalTemplate, org.key_project.logic.ChoiceExpr>) goal2Choices
+                        .clone();
+        return rb;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/FindTacletBuilder.java

@@ -41,7 +41,7 @@ public abstract class FindTacletBuilder<T extends FindTaclet> extends TacletBuil
      * exception otherwise
      */
     protected void checkBoundInIfAndFind() {
-        final BoundUniquenessChecker ch = new BoundUniquenessChecker(getFind(), ifSequent());
+        final BoundUniquenessChecker ch = new BoundUniquenessChecker(getFind(), assumesSequent());
         if (!ch.correct()) {
             throw new TacletBuilderException(this,
                 "A bound SchemaVariable variables occurs both " + "in assumes and find clauses.");

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/NoFindTacletBuilder.java

@@ -60,7 +60,7 @@ public void addTacletGoalTemplate(TacletGoalTemplate goal) {
      * an exception otherwise
      */
     protected void checkBoundInIfAndFind() {
-        final BoundUniquenessChecker ch = new BoundUniquenessChecker(ifSequent());
+        final BoundUniquenessChecker ch = new BoundUniquenessChecker(assumesSequent());
         if (!ch.correct()) {
             throw new TacletBuilderException(this, "A bound SchemaVariable occurs twice in if.");
         }
@@ -80,4 +80,18 @@ public NoFindTaclet getTaclet() {
         checkBoundInIfAndFind();
         return getNoFindTaclet();
     }
+
+    @Override
+    public NoFindTacletBuilder copy() {
+        var rb = new NoFindTacletBuilder();
+        rb.setAnnotations(tacletAnnotations);
+        rb.setAssumesSequent(assumesSeq);
+        rb.setChoices(choices);
+        rb.setDisplayName(attrs.displayName());
+        rb.setName(name);
+        rb.setTacletGoalTemplates(goals);
+        rb.setTrigger(attrs.trigger());
+        rb.setRuleSets(ruleSets);
+        return rb;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilder.java

@@ -92,4 +92,34 @@ public void addGoalTerm(JTerm goalTerm) {
     public T getTaclet() {
         return getRewriteTaclet();
     }
+
+    @Override
+    public RewriteTacletBuilder<T> copy() {
+        var rb = new RewriteTacletBuilder<T>().setFind((JTerm) getFind());
+        rb.setSurviveSmbExec(surviveSmbExec);
+        rb.setAnnotations(tacletAnnotations);
+        rb.setApplicationRestriction(applicationRestriction);
+        rb.setAssumesSequent(assumesSeq);
+        rb.setChoices(choices);
+        rb.setDisplayName(attrs.displayName());
+        rb.setName(name);
+        rb.setTacletGoalTemplates(goals);
+        rb.setTrigger(attrs.trigger());
+        rb.setRuleSets(ruleSets);
+        for (var vc : variableConditions) {
+            rb.addVariableCondition(vc);
+        }
+        rb.addVarsNew(varsNew);
+        rb.addVarsNotFreeIn(varsNotFreeIn);
+        for (var vc : varsNewDependingOn) {
+            rb.addVarsNewDependingOn(vc.first(), vc.second());
+        }
+        rb.setFind((JTerm) find);
+        rb.setChoices(choices);
+        if (goal2Choices != null)
+            rb.goal2Choices =
+                (java.util.HashMap<TacletGoalTemplate, org.key_project.logic.ChoiceExpr>) goal2Choices
+                        .clone();
+        return rb;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilderSchemaVarCollector.java

@@ -35,7 +35,8 @@ public RewriteTacletBuilderSchemaVarCollector(
 
     public Set<SchemaVariable> collectSchemaVariables() {
 
-        Set<SchemaVariable> result = new LinkedHashSet<>(collectSchemaVariables(rtb.ifSequent()));
+        Set<SchemaVariable> result =
+            new LinkedHashSet<>(collectSchemaVariables(rtb.assumesSequent()));
 
         if (rtb instanceof FindTacletBuilder) {
             result.addAll(collectSchemaVariables(rtb.getFind()));

key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/SuccTacletBuilder.java

@@ -90,4 +90,33 @@ public SuccTaclet getSuccTaclet() {
     public SuccTaclet getTaclet() {
         return getSuccTaclet();
     }
+
+    @Override
+    public SuccTacletBuilder copy() {
+        var rb = new SuccTacletBuilder().setFind((Sequent) getFind());
+        rb.setAnnotations(tacletAnnotations);
+        rb.setApplicationRestriction(applicationRestriction);
+        rb.setAssumesSequent(assumesSeq);
+        rb.setChoices(choices);
+        rb.setDisplayName(attrs.displayName());
+        rb.setName(name);
+        rb.setTacletGoalTemplates(goals);
+        rb.setTrigger(attrs.trigger());
+        rb.setRuleSets(ruleSets);
+        for (var vc : variableConditions) {
+            rb.addVariableCondition(vc);
+        }
+        rb.addVarsNew(varsNew);
+        rb.addVarsNotFreeIn(varsNotFreeIn);
+        for (var vc : varsNewDependingOn) {
+            rb.addVarsNewDependingOn(vc.first(), vc.second());
+        }
+        rb.setFind((Sequent) find);
+        rb.setChoices(choices);
+        if (goal2Choices != null)
+            rb.goal2Choices =
+                (java.util.HashMap<TacletGoalTemplate, org.key_project.logic.ChoiceExpr>) goal2Choices
+                        .clone();
+        return rb;
+    }
 }