Clean up inheritance

KeYProject · May 22, 2024 · 9d5cabc · 9d5cabc
1 parent 6ae7e2a
commit 9d5cabc
Show file tree

Hide file tree

Showing 10 changed files with 31 additions and 46 deletions.
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
@@ -164,9 +164,4 @@ protected MatchConditions matchChildren(SourceData source, MatchConditions match
 
         return matchCond;
     }
-
-    @Override
-    public SyntaxElement getChild(int n) {
-        return getChildAt(n);
-    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/NonTerminalProgramElement.java
@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.java;
 
+import org.key_project.logic.SyntaxElement;
+
 /**
  * Non terminal program element. taken from COMPOST and changed to achieve an immutable structure
  */
@@ -25,4 +27,8 @@ public interface NonTerminalProgramElement extends ProgramElement {
      */
     ProgramElement getChildAt(int index);
 
+    @Override
+    default SyntaxElement getChild(int n) {
+        return getChildAt(n);
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java b/key.core/src/main/java/de/uka/ilkd/key/java/TerminalProgramElement.java
@@ -4,19 +4,12 @@
 package de.uka.ilkd.key.java;
 
 import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.TerminalSyntaxElement;
 
 /**
  * Terminal program element. taken from COMPOST and changed to achieve an immutable structure
  */
 
-public interface TerminalProgramElement extends ProgramElement {
-    @Override
-    default int getChildCount() {
-        return 0;
-    }
+public interface TerminalProgramElement extends ProgramElement, TerminalSyntaxElement {
 
-    @Override
-    default SyntaxElement getChild(int n) {
-        throw new IndexOutOfBoundsException("Program element " + this + " has no children");
-    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/Modifier.java
@@ -7,13 +7,14 @@
 import de.uka.ilkd.key.java.TerminalProgramElement;
 import de.uka.ilkd.key.java.visitor.Visitor;
 
+import org.key_project.logic.SyntaxElement;
 import org.key_project.util.ExtList;
 
 /**
  * Modifier. taken from COMPOST and changed to achieve an immutable structure
  */
 
-public abstract class Modifier extends JavaProgramElement implements TerminalProgramElement {
+public abstract class Modifier extends JavaProgramElement {
 
     /**
      * Modifier.
@@ -56,4 +57,14 @@ public String getText() {
     public void visit(Visitor v) {
         v.performActionOnModifier(this);
     }
+
+    @Override
+    public int getChildCount() {
+        return 0;
+    }
+
+    @Override
+    public SyntaxElement getChild(int n) {
+        throw new IndexOutOfBoundsException(getClass() + " " + this + " has no children");
+    }
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java b/key.core/src/main/java/de/uka/ilkd/key/java/declaration/modifier/Static.java
@@ -5,6 +5,7 @@
 
 import de.uka.ilkd.key.java.declaration.Modifier;
 
+import org.key_project.logic.TerminalSyntaxElement;
 import org.key_project.util.ExtList;
 
 /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/IForUpdates.java
@@ -7,7 +7,7 @@
 
 import org.key_project.util.collection.ImmutableArray;
 
-public interface IForUpdates extends de.uka.ilkd.key.java.TerminalProgramElement {
+public interface IForUpdates extends de.uka.ilkd.key.java.NonTerminalProgramElement {
 
     int size();
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java b/key.core/src/main/java/de/uka/ilkd/key/java/statement/ILoopInit.java
@@ -4,11 +4,12 @@
 package de.uka.ilkd.key.java.statement;
 
 import de.uka.ilkd.key.java.LoopInitializer;
+import de.uka.ilkd.key.java.NonTerminalProgramElement;
 import de.uka.ilkd.key.java.TerminalProgramElement;
 
 import org.key_project.util.collection.ImmutableArray;
 
-public interface ILoopInit extends TerminalProgramElement {
+public interface ILoopInit extends NonTerminalProgramElement {
 
     int size();
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
@@ -34,7 +34,7 @@
  * Objects of this class are schema variables matching program constructs within modal operators.
  * The particular construct being matched is determined by the ProgramSVSort of the schema variable.
  */
-public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator , TerminalSyntaxElement {
+public final class ProgramSV extends OperatorSV implements ProgramConstruct, UpdateableOperator , SyntaxElement {
     public static final Logger LOGGER = LoggerFactory.getLogger(ProgramSV.class);
 
     private static final ProgramList EMPTY_LIST_INSTANTIATION =
@@ -150,12 +150,12 @@ public ProgramElement getChildAt(int index) {
 
     @Override
     public SyntaxElement getChild(int n) {
-        return TerminalSyntaxElement.super.getChild(n);
+        throw new IndexOutOfBoundsException("ProgramSV " + this + " has no children");
     }
 
     @Override
     public int getChildCount() {
-        return TerminalSyntaxElement.super.getChildCount();
+        return 0;
     }
 
     @Override

diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java b/key.core/src/main/java/de/uka/ilkd/key/logic/op/Qualifier.java
@@ -6,8 +6,9 @@
 import java.util.WeakHashMap;
 
 import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.TerminalSyntaxElement;
 
-public class Qualifier<T> implements SyntaxElement {
+public class Qualifier<T> implements TerminalSyntaxElement {
     private final T qualifier;
 
     private static final WeakHashMap<Object, Qualifier<?>> INSTANCES = new WeakHashMap<>();
@@ -28,14 +29,4 @@ synchronized static <T> Qualifier<T> create(T qualifier) {
     public T getQualifier() {
         return qualifier;
     }
-
-    @Override
-    public SyntaxElement getChild(int n) {
-        return null;
-    }
-
-    @Override
-    public int getChildCount() {
-        return 0;
-    }
 }
diff --git a/key.ncore/src/main/java/org/key_project/logic/op/Modality.java b/key.ncore/src/main/java/org/key_project/logic/op/Modality.java
@@ -5,10 +5,7 @@
 
 import java.util.Objects;
 
-import org.key_project.logic.Name;
-import org.key_project.logic.Named;
-import org.key_project.logic.Program;
-import org.key_project.logic.SyntaxElement;
+import org.key_project.logic.*;
 import org.key_project.logic.sort.Sort;
 
 /**
@@ -58,7 +55,7 @@ public SyntaxElement getChild(int n) {
     /**
      * Modality kinds like box and diamond.
      */
-    public abstract static class Kind implements Named, SyntaxElement {
+    public abstract static class Kind implements Named, TerminalSyntaxElement {
         private final Name name;
 
         public Kind(Name name) {
@@ -88,15 +85,5 @@ public boolean equals(Object o) {
         public int hashCode() {
             return Objects.hash(name());
         }
-
-        @Override
-        public int getChildCount() {
-            return 0;
-        }
-
-        @Override
-        public SyntaxElement getChild(int n) {
-            throw new IndexOutOfBoundsException("Modality kind " + name() + " has no children");
-        }
     }
 }