Remove id from ProductionReference and store in Map instead.

kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java

@@ -66,6 +66,7 @@ public enum Status {
   private final boolean debug;
   private final Module mod;
   private final java.util.Set<SortHead> sorts;
+  private final Map<ProductionReference, Integer> prIds = new IdentityHashMap<>();
 
   // logic QF_DT is best if it exists as it will be faster than ALL. However, some z3 versions do
   // not have this logic.
@@ -593,15 +594,15 @@ public String apply(Term t) {
       boolean isTopSort =
           expectedSort.equals(Sorts.RuleContent()) || expectedSort.name().equals("#RuleBody");
       int id = nextId;
-      boolean shared = pr.id().isPresent() && variablesById.size() > pr.id().get();
+      boolean shared = prIds.containsKey(pr) && variablesById.size() > prIds.get(pr);
       if (!shared) {
         // if this is the first time reaching this term, initialize data structures with the
         // variables associated with
         // this term.
         nextId++;
         variablesById.add(new ArrayList<>());
         cacheById.add(new HashSet<>());
-        pr.setId(Optional.of(id));
+        prIds.put(pr, id);
         for (Sort param : iterable(pr.production().params())) {
           String name = "FreshVar" + param.name() + locStr(pr);
           if (!variables.contains(name)) {
@@ -612,7 +613,7 @@ public String apply(Term t) {
         }
       } else {
         // get cached id
-        id = pr.id().get();
+        id = prIds.get(pr);
       }
       if (pr instanceof TermCons tc) {
         boolean wasStrict = isStrictEquality;
@@ -682,7 +683,7 @@ public String apply(Term t) {
             nextId++;
             variablesById.add(new ArrayList<>());
             cacheById.add(new HashSet<>());
-            pr.setId(Optional.of(id));
+            prIds.put(pr, id);
             if (isAnonVar(c)) {
               name = "Var" + c.value() + locStr(c);
               isStrictEquality = true;
@@ -799,7 +800,7 @@ private String printSort(Sort s, Optional<ProductionReference> t, boolean isIncr
     Map<Sort, String> params = new HashMap<>();
     if (t.isPresent()) {
       if (t.get().production().params().nonEmpty()) {
-        int id = t.get().id().get();
+        int id = prIds.get(t.get());
         List<String> names = variablesById.get(id);
         Seq<Sort> formalParams = t.get().production().params();
         assert (names.size() == formalParams.size());
@@ -945,8 +946,8 @@ void pushNotModel() {
   }
 
   public Seq<Sort> getArgs(ProductionReference pr) {
-    if (pr.id().isPresent()) {
-      int id = pr.id().get();
+    if (prIds.containsKey(pr)) {
+      int id = prIds.get(pr);
       List<String> names = variablesById.get(id);
       return names.stream().map(this::getValue).collect(Collections.toList());
     } else {
@@ -1023,7 +1024,7 @@ private void reset() {
     }
   }
 
-  private static String locStr(ProductionReference pr) {
+  private String locStr(ProductionReference pr) {
     String suffix = "";
     if (pr.production().klabel().isDefined()) {
       suffix = "_" + pr.production().klabel().get().name().replace("|", "");
@@ -1040,7 +1041,7 @@ private static String locStr(ProductionReference pr) {
           + l.endColumn()
           + suffix;
     }
-    return pr.id().get() + suffix;
+    return prIds.get(pr) + suffix;
   }
 
   private StringBuilder sb = new StringBuilder();

kore/src/main/scala/org/kframework/parser/treeNodes.scala

@@ -2,14 +2,14 @@
 
 package org.kframework.parser
 
-import org.kframework.attributes.{Source, Location, HasLocation}
+import org.kframework.attributes.{HasLocation, Location, Source}
 import org.kframework.definition.Production
 import org.kframework.kore.KORE.Sort
-import java.util._
-import org.pcollections.{ConsPStack, PStack}
-import collection.JavaConverters._
 import org.kframework.utils.StringUtil
+import org.pcollections.{ConsPStack, PStack}
 
+import java.util._
+import scala.collection.JavaConverters._
 import scala.collection.mutable
 
 trait Term extends HasLocation {
@@ -19,11 +19,6 @@ trait Term extends HasLocation {
 
 trait ProductionReference extends Term {
   val production: Production
-  var id: Optional[Integer] = Optional.empty()
-
-  def setId(id: Optional[Integer]): Unit = {
-    this.id = id
-  }
 }
 
 trait HasChildren {
@@ -46,10 +41,10 @@ case class TermCons private (items: PStack[Term], production: Production)
   def get(i: Int): Term = items.get(items.size() - 1 - i)
 
   def `with`(i: Int, e: Term): TermCons =
-    TermCons(items.`with`(items.size() - 1 - i, e), production, location, source, id)
+    TermCons(items.`with`(items.size() - 1 - i, e), production, location, source)
 
   def replaceChildren(newChildren: java.util.Collection[Term]): TermCons =
-    TermCons(ConsPStack.from(newChildren), production, location, source, id)
+    TermCons(ConsPStack.from(newChildren), production, location, source)
 
   override def toString: String = new TreeNodesToKORE(s => Sort(s)).apply(this).toString()
 
@@ -84,25 +79,14 @@ object TermCons {
       items: PStack[Term],
       production: Production,
       location: Optional[Location],
-      source: Optional[Source],
-      id: Optional[Integer]
+      source: Optional[Source]
   ): TermCons = {
     val res = TermCons(items, production)
     res.location = location
     res.source = source
-    res.id = id
     res
   }
 
-  def apply(
-      items: PStack[Term],
-      production: Production,
-      location: Optional[Location],
-      source: Optional[Source]
-  ): TermCons = {
-    TermCons(items, production, location, source, Optional.empty())
-  }
-
   def apply(
       items: PStack[Term],
       production: Production,
@@ -112,9 +96,7 @@ object TermCons {
     items,
     production,
     Optional.of(location),
-    Optional.of(source),
-    Optional
-      .empty()
+    Optional.of(source)
   )
 }